Home » forums » LtU Forum

obj vs. ml vs. coq (fight?)

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.

By raould at 2010-09-27 23:30 | LtU Forum | previous forum topic | next forum topic | other blogs | 6156 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Coq is not a traditionnal programming language

In the sense that it does not supply many of the standard tools that more widely used, less experimental languages provide input-output, file manipulation, advanced features like macros and GC options, etc.

In a sense, Coq can be seen to live in the intersection of OCaml, Haskell and Scheme, as far as standard programming features are concerned. This is what makes extraction to these languages (relatively) easy. In short, even if for some reason you wanted to write a program that could compile to these three languages, I doubt Coq would be the way to go. Also keep in mind that there is no formal check that the semantics of the "translated" code corresponds to that of the original Coq code (though quite some work has been made in that direction).

By codyroux at Tue, 2010-09-28 13:08 | login or register to post comments

Macros

Coq actually has better support for "macros" than any other statically-typed functional language that I'm aware of. They're just called "notations" instead.

By Adam Chlipala at Tue, 2010-10-05 14:48 | login or register to post comments

codyroux is right...

...but with respect to "every change requires tedious adjustments of the proofs," it's worth noting the work of Adam Chlipala and others on making extensive use of Coq's support for proof automation to mitigate this, with some impressive results, e.g. in Ynot.

By Paul Snively at Tue, 2010-09-28 18:35 | login or register to post comments