[FOM] Kenzo software finds error in published homotopy theorem
freek at cs.ru.nl
Fri Nov 7 05:55:04 EST 2014
>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.
More information about the FOM