What is the single 'one object' that an interpreter, compiler, abstract interpreter, symbolic executor and prover are all views of?	A program's behavior — extensionally, a partial function Program × Input ⇀ Output, equivalently a relation, or a set of execution traces. Every tool reads a description of this one object and reports something true about it.
Two tools both report true things about a program but say different things ('exactly 6' vs 'positive'). Why is that not a contradiction?	They sit at different rungs of a precision lattice. Coarser answers contain the truth rather than conflicting with it: 6 is positive, 6 is even, 6 ∈ [1,∞], 6 ∈ ⊤ are all sound. A sound abstract view is never wrong — only, by design, vague.
Why is 'these tools won't contradict each other' a theorem rather than a gift?	If two tools literally share the same semantics generator, agreement is automatic. The moment they read different descriptions, agreement must be earned by a linking theorem (equivalence, adequacy, simulation, Galois soundness, conformance). Skip the theorem and you get drift.
Curry–Howard makes 'a theorem prover' coherent as a kind of program. What is the slogan, and what operation does it identify?	Proofs-as-programs, propositions-as-types: a proof is a program, a proposition is a type. So 'checking a proof' and 'type-checking a program' are literally the same operation — which is why a proof checker can be a tiny trusted kernel.