alpheccar's blog - tag ocaml http://www.alpheccar.org en 40 science and freedom http://www.alpheccar.org alpheccar's blog - tag ocaml http://www.alpheccar.org/images/avatar.jpg Djinn, Coq, Monad and a bit of Haskell 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/).

Read More...

]]> Thu, 24 May 2007 14:18:57 -0500 urn:uuid:65 webmaster@alpheccar.org http://www.alpheccar.org/en/posts/show/70 http://www.alpheccar.org/en/posts/show/70#comments haskell ocaml coq djinn The best programming languages It is of course impossible to choose, in a objective and absolute way the best programming language. Choosing a programming language is dependent on too many things. A language which may be very good for a specific use may be the wrong language to use for another task.

Read More...

]]> Tue, 13 Jun 2006 11:47:55 -0500 urn:uuid:37 webmaster@alpheccar.org http://www.alpheccar.org/en/posts/show/36 http://www.alpheccar.org/en/posts/show/36#comments programming language ruby haskell python lisp smalltalk ocaml