3 ms·

disclaimer: outside of a quick understanding of what "formal proof system" is, I have no deep understanding of how it works. It is written there's a Coq->OCaml

by allan_s 12y ago

disclaimer: outside of a quick understanding of what "formal proof system" is, I have no deep understanding of how it works. It is written there's a Coq->OCaml compilation step. Would it be easily possible to have any Coq->other language (I'm mostly thinking about Rust) compiler ? Or do some properties of OCaml make it much easier (I mean "several order of magnitude") to implement than more 'common' dynamic languages like Php/Python/ruby ?

sun_machine 12y ago
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.
- allan_s 12y ago
  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 ?
  - clarus 12y ago
    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/Computation.v https://github.com/clarus/coq-chick-blog/blob/master/Computa... and https://github.com/clarus/coq-chick-blog/blob/master/Extraction.v https://github.com/clarus/coq-chick-blog/blob/master/Extract...
adultSwim 12y ago
It's definitely possible. The hand wavy version is that basically you just throw out all the fancy types, throw out all the proofs, and just leave the data and functions. So let's say in Coq I write a sorting function. In Coq it could have a type where it takes a list and returns the same list sorted (i.e. proven that it works). I can extract to OCaml and be just left with a function which a type that takes a list and returns a list. However the computation being done is still the same. The target language doesn't even need types. I don't know if it's still maintained but there used to be an extraction back-end to Scheme (also one for Haskell). Being a functional language makes things much easier. Need to have something to map algebraic data types, functions, and function application.
- pseudonom- 12y ago
  My understanding is that, after translation, Agda's Haskell makes rather liberal use of unsafeCoerce :: a -> b (it's already been type checked by Agda, after all).
  - vilhelm_s 12y ago
    Yes, that's true for Coq extraction also. You can choose to extract to ML, Haskell or Scheme, but whichever one you pick the target language is basically treated as an untyped language. (Of course, it tries to avoid unsafeCoerce/Obj.magic if possible; if the program can be typed with just simple types, the extracted code should not have any unsafe coercions in it.)

by allan_s 12y ago

sun_machine 12y ago

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.

allan_s 12y ago
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 ?
- clarus 12y ago
  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/Computation.v https://github.com/clarus/coq-chick-blog/blob/master/Computa... and https://github.com/clarus/coq-chick-blog/blob/master/Extraction.v https://github.com/clarus/coq-chick-blog/blob/master/Extract...

adultSwim 12y ago

It's definitely possible. The hand wavy version is that basically you just throw out all the fancy types, throw out all the proofs, and just leave the data and functions. So let's say in Coq I write a sorting function. In Coq it could have a type where it takes a list and returns the same list sorted (i.e. proven that it works). I can extract to OCaml and be just left with a function which a type that takes a list and returns a list. However the computation being done is still the same. The target language doesn't even need types. I don't know if it's still maintained but there used to be an extraction back-end to Scheme (also one for Haskell). Being a functional language makes things much easier. Need to have something to map algebraic data types, functions, and function application.

pseudonom- 12y ago
My understanding is that, after translation, Agda's Haskell makes rather liberal use of unsafeCoerce :: a -> b (it's already been type checked by Agda, after all).
- vilhelm_s 12y ago
  Yes, that's true for Coq extraction also. You can choose to extract to ML, Haskell or Scheme, but whichever one you pick the target language is basically treated as an untyped language. (Of course, it tries to avoid unsafeCoerce/Obj.magic if possible; if the program can be typed with just simple types, the extracted code should not have any unsafe coercions in it.)