News for hackers. Stuff that matters.

A comment on A blog engine written and proven in Coq. Parent comment

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 ?
[ Parent | on HN ]
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...

[ Parent | on HN ]