[FOM] Formal verification

[Freek Wiedijk]

Dear Harvey,

>This is, of course, a totally unacceptable ugly piece
>of disgusting garbage (smile), according to any current
>standards of mathematical practice.

In what sense?  Syntactically it looks like a programming
language, yes, but I don't consider that a big problem.
Yes, people sometimes work on making things look nicer on
the surface.  But I don't think that _that's_ the bottleneck
for formalization technology.

It's like the difference between Word and LaTeX.  I don't
mind working in LaTeX either.  And this Agda proof that the
HoTT people like so much looks like a compute program just
the same (Agda _is_ a programming language.)

But I find it very interesting that you have this reaction.
It's exactly what Henk always tells me when he's looking
at a proof script I'm showing him.

_Conceptually_ this formalization is not so bad, I think.
If _that_ is what you mean by not being up to the standards
of mathematical practice, I think I disagree.  In a couple
of lines it proves a statement like

  (!x. f contl x) /\
  (!x. f x > x) /\
  (!n. x (n + 1) = f (x n))
  ==> !y. ?n. x n > y

in the HOL logic.  _Really_ proving it, all the way from
the three HOL axioms using the ten HOL proof rules.  Nothing
assumed without proof.  I didn't count the inference steps
that my piece of code runs through the HOL Light kernel,
but I guess it will have been a couple of thousands.

So this statement is just plain ASCII too.  You should read
the "!" as the universal quantifier, "?" as the existential
quantifier, "f contl x" as "f is continuous in x", etc.
I kind of like the HOL Light statement language (but then
I'm a Unix/Perl kind of person :-))

Incidentally, the "De Bruijn factor" (the ratio between
informal and formal versions) of this example is 1.4.
Which is not that bad, I think.

>Incidentally, this is a kind of beautiful example, I think
>just meaty enough to be interesting.

I know the HIT that in HoTT represents the circle, but what
is the HIT for the real line?  Or is in HoTT the real line
the same thing as the one point space?  (They have the
same _homotopy,_ but surely these are different things?
For one thing, there is more than one real number, right?)

Freek