[FOM] Computational set theory

[Freek Wiedijk]

Hi Henk,

>But then one has to introduce a functional programming language
>within ZF. And to run such a
>program (of say an efficient primality test) one essentially needs to
>write a compiler, because
>at the end one doesn't like to rely on someone else's software.

If I run Coq, I'm relying on someone else's software too :-)
The Coq kernel is _huge,_ you know.  (I always used to claim
that the Coq kernel is larger than the full Mizar system.
It is not true.  But they are close.)

If I would move to a foundations ZFC+PP (where PP means
"Poincaré principle": I add one proof rule that gives me the
calculations in my functional programming language for free,
without having to "prove" them from the ZFC axioms), would
you consider that to be inferior to the way the Poincaré
principle works in type theory?  The size of the trusted
code base ("someone else's software") probably would be
quite a bit smaller than the Coq kernel, in such a system?

More interestingly: let's fast forward to the future, and
imagine a system like the CakeML effort by Magnus Myreen,
Ramana Kumar, Scott Owens and Michael Norrish.  I.e.,
a HOL implementation, where the ML running that system is
fully verified inside the system itself all the way from
the syntax to the machine code, and where the HOL kernel
also has been fully proved correct.  Everything would be
very much fully verified and bootstrapping in such a system.

Now, we can imagine that instead of proving that a program
in this pervasive ML language (the implementation language
of the system, the output language of the program extraction)
evaluates to a certain value, instead of doing this from the
semantics inside the HOL logic (which _is_ possible), the
kernel of such a system allows one to "cheat".  Just _run_
the program, and use the output of it to synthesize this
evaluation theorem.

Wouldn't that be nice? :-)  While of course in that case
you morally still don't have any evaluation of functional
programs in your foundations.

Freek