News for hackers. Stuff that matters.
Re:A blog engine written and proven in Coq by clarus on Friday February 13, 2015 @06:20AM (#9043792)
Coq itself is already a programming language, but pure in the sense there cannot be any side effects (like IOs). For this pure part there are already an interpreter and a compiler to OCaml, Haskell or Scheme.

To extend Coq with IOs you need to define each new external call. This is basically what is done in the files https://github.com/clarus/coq-chick-blog/blob/master/Computa... and https://github.com/clarus/coq-chick-blog/blob/master/Extract...

There are no comments on this comment yet.