Tag : coq

Before continuing my exploration of the specification and extraction of softwares in Coq, I think I should make a pause and focus a little on Coq basics like the differences between Set and Prop and the meaning of a type like 4>0 ...

Even if your are a beginner in functional programming, you have probably heard of the program-as-proof correspondence, also known as the Curry-Howard isomorphism. It is a bridge between the world of logic and the world of computation. A type is a specification and a program is a proof of that type. Typechecking is just checking the proof. Types can be used to specify lots of constraints about your programs. With sophisticated type systems like the ones in [Ocaml](http://caml.inria.fr/ocaml/index.fr.html) and [Haskell](http://haskell.org/haskellwiki/Haskell) you can really do wonderful stuff. But, those type systems are not powerful enough. We may dream of extracting a program from its specification. But, for that we need to be able to express very rich specifications. It is possible with the calculus of constructions which is the type system implemented in [Coq](http://coq.inria.fr/).

After my two previous posts about Coq, I am now ready to write a little about strong specification in Coq. A strongly specified function is a function which is containing its specification in its output type.