Jason (jcreed) wrote,

I went to this talk by Tom Hales yesterday — it wasn't all that noteworthy to me in particular since I had basically seen the same talk before, but the gist of it is that he takes very seriously the idea of mechanization of formal proofs in ordinary work-a-day mathematics, which is very cool. He started out as an "ordinary" mathematician working on the Kepler Conjecture. When his (partially computer-calculation-based) proof of the conjecture stalled for years in the journal peer-review process and eventually was merely "accepted" as being only as strong as experimental evidence because none of the reviewers actually felt capable of checking the correctness of his code, he set off on formalizing the whole damn thing.

Anyhow, it just reminded me of HOL-Light, the tool he uses to do his formalization in, and how simple it is supposed to be for having only a 1,000 loc "trusted computing base", that being a 1,000 line C program, I think. It got me wondering how much effort and code it would really take, comparatively, to hack up just a canonical-forms LF typechecker, a task whose easiness has long been a rule of thumb, and it turned out the thumb was right. About two hours of hacking, and 125 lines of ML. It even fits on one screen if I take out all the whitespace:

It's probably not very efficient at all, since I implemented contexts and signatures very naively, and it has a funny input syntax to make parsing relatively trivial. Still, proof of concept.
Tags: lf, programming
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded