Lambda the Ultimate

the omega thread had me re-perusing the web about things like coq, and i noticed it can extract to haskell, ocaml, or scheme. which got me wondering if it could be a daily programming tool that would help give some portability to the shipped executables. a scary route to get there, but maybe interesting. then i found a paper talking about that a bit:

The question arises of which language is best suited for fast prototyping. If no verification is needed, the answer would probably be ML. ... A consequence [in Coq] is that every change requires tedious adjustments of the proofs.

er - not surprising conclusion, i guess.