A compiler defines the meaning of the language it is written in. The fixed point, what it cannot prove — and Gödel.
On the left, selfie.c: text, 365,784 characters. On the right, what the machine does when it runs. The arrow between them is starc, the compiler — and starc's own source code is in the left box.
That is a dictionary written in the language it defines. In English it would be a paradox. Here it is not, and the difference is that the definition is executable: a machine can run the dictionary.
Week 4 fixed meaning by decree. This is the decree, and it is a program.
Scanner. Characters into symbols — the 22 symbols and 7 keywords of week 4. A finite state machine, one per kind of symbol.
Parser. Symbols against the grammar. A successful parse is a derivation, which is a proof that the text is a C* program. It always terminates and always answers. Syntax is decidable.
Code generator. For each construct, the RISC-U instructions that mean it: the nine lines of week 4's loop. This is where meaning is made, and it is the only place.
Exactly one thing: that selfie agrees with itself. A compiler that consistently mistranslated one construct would reproduce the mistake perfectly, and pass.
It does not prove that selfie is correct. It does not prove that selfie.c is what compiled selfie. The source does not determine the binary.
Ken Thompson's Turing award lecture. A compiler that recognises when it is compiling the login program and inserts a back door — and recognises when it is compiling a compiler, and inserts the code that does both.
Remove the trick from the compiler's source. Recompile with the infected compiler. The back door survives, because the source is not what compiled the compiler. Every line inspected and found clean; the binary still lies.
You can't trust code that you did not totally create yourself.Ken Thompson, Reflections on Trusting Trust
Compile the compiler with two unrelated compilers and compare the results — David Wheeler, 2005. The check that the fixed point cannot supply comes from outside the loop. Remember the shape.
How. Build, by Gödel numbering, a sentence that says: "this sentence has no proof in this system." If it were provable, the system proves a falsehood. So it is unprovable — and therefore true.
The same diagonal. Cantor built a row not on the list. Gödel builds a truth not on the list of provable things. Adding it as a new axiom does not help: the construction simply runs again.
Proof is a finite object you can check. Truth is not. Proof is syntax. Truth is semantics. They are not the same size — and week 7 already knew that. Gödel says where to look.
A trustworthy system cannot be the source of its own trust. Confidence has to come from outside: a stronger theory, an experiment, an independent compiler, reality.
When a machine explains why its own answer is correct, you have received more output from the same machine — fluent, plausible, and not a certificate. Introspection is not audit.
Tarski, 1936, closes the circle: no sufficiently expressive language can define truth for its own sentences. Truth always lives one level up.
The first is about the text: the parser decided it, always, in finite time. The second is about the text too — a type is a label the compiler attached — so it is decided, and only a warning because C* is permissive.
The third is about behaviour. The compiler said nothing. The machine found it, on this run, on this input. Next week: why no compiler can ever say it in general — and why that is fine.
Self-reference II: will this program ever stop? No program can always tell. Then the same move run forwards — one machine that can be any machine — and Rice: every interesting question about behaviour.