[FOM] Proof Assistants and Conjectures (reply to Chow)

[Vaughan Pratt]

Brian Hart wrote:
>> Not that this necessarily makes the definition any easier, Goedel
>> had quite a struggle formulating his incompleteness theorems.
>>
>> Vaughan Pratt
> 
> Can you be more specific?

If you think Goedel numbers are easy, try coding them yourself.  You'll 
soon understand what Goedel was up against.  Bear in mind that unlike 
you, neither Goedel nor anyone else had ever seen a complex program 
before.  Goedel had to figure out not only the intricate coding details 
of both his interpreter and the datastructures it was going to operate 
on, but the entire computational paradigm for what he was doing, which 
was at that time completely nonexistent.  What could it even mean to 
write an interpreter of programs in a logical language that is used 
simultaneously to code the programs it is interpreting?  The whole 
concept is utterly preposterous for anyone who hasn't seen how these 
ideas can come together in a way that actually makes sense.  This was an 
utterly mind-boggling accomplishment for its time.

Vaughan Pratt