[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

There is also Peter Hancock's question. Well, probably not a question. 
But I lost your message, Peter, and I can't find it.

My quibble with the so-called Church's Thesis in constructive 
mathematics is that ... I never need it when I prove a theorem. Knowing 
that my input is computable doesn't help me in my calculations. I have 
no need to inspect the source code of the input, or of merely knowing 
that the source code exists.

Moreover, I would think that many inputs come without evidence of 
computability.

Example 1. Suppose I program a certified web server in Agda. My input is 
a stream, and so is my output. If I assumed CT, the protocol would have 
to work like this: please, before sending me the stream, send me its 
Godel number, or promise that it secretly exists, and send me evidence 
of your promise.

Example 2. Suppose I program a certified flight control system for 
airports. Again my input and output are streams. Assuming that the 
inputs come with their Godel numbers, there is no need for radars or 
other tracking devices. I can compute what will happen from the Godel 
number, and I can effectively predict which planes will be where and 
when by just computing. Wouldn't that be marvelous?

Example 3. Suppose I program a certified nuclear power station control 
system. One of my stream inputs comes from a Geiger counter. I ask the 
physicists and engineers to design and build an improved Geiger counter 
that first gives the Godel number of the sequence that it produces.

What do you need to know that your input if computable for? And what if 
your input is not (known to be) computable?

Should you implement a validation procedure that rejects non-computable 
input?

Martin