[FOM] Kenzo software finds error in published homotopy theorem

[Freek Wiedijk]

Dear Tim,

>What about Kenzo?  Rewriting it so that its results are formally
>correct must incur a computational cost.  Is it possible to estimate
>how much of a slowdown that would be?

It depends on the framework you would use, I guess?

If you would do it in Coq, and would do it properly, it
would be of OCaml speed.  So I guess the speed difference
would then be that of an industrial strength Common Lisp
(Kenzo) and OCaml (extracted OCaml, or even inside Coq).

If I google a bit, I get the impression that these two
languages are of a similar performance!  That surprises me,
I would have guessed Common Lisp to be the faster of the two.

As a start in this direction, while contemplating a port
of Kenzo along the path

	Common Lisp -> OCaml -> Coq

I ported a fragment of Kenzo to OCaml.  It corresponds to
the first two chapters of the manual.  Yes, I really also
should have done chapter 3, with the Smith normal form
calculations, but I got bored/distracted.

The port was very straightforward, though, if anyone wants
a copy of the about a thousand lines of OCaml that I wrote,
just mail me.

Freek