Re:A blog engine written and proven in Coq
by sun_machine on Thursday February 12, 2015 @11:04AM
(#9039369)
Coq is essentially a verification system and functional programming language all in one. The functional programming language that the proofs are based on has similar (identical in some places) semantics to OCaml. Remaining faithful to these semantics, especially in a verifiable way, quickly becomes herculean. Even formalizing the semantics of a language is a process that takes months.
[ Parent
| on HN ]
Re:A blog engine written and proven in Coq
by allan_s on Thursday February 12, 2015 @11:10AM
(#9039401)
I understand better, so basically before doing anything you will first need to define what each "part" of the language "means" in term of "logical operation" (like what does the dot operator '.' means in PHP, which type it accepts and it transforms them etc) Right ?
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...