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.

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 and 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.

This weekend, I wanted to do some experimentations with random number generations and arrays in Haskell. So, I decided to build a small Iterated Function System (IFS) library because it is a quite standard stuff, easy and which can generate some cool pictures. And, it needs random number generation, array and speed.

I have recently convinced one of my friends to learn Haskell. But, he finds it very difficult. He is making a big effort and really wants to learn it but the beginning is hard and he may have spent too much time writing Java code.

So, to help him, I have written a short Haskell study plan. It may interest some other people so I decided to take the risk to post it on my blog. It is very informal and subjective but I think it is a good summary of the problems I had to solve myself to learn Haskell. So, when reading the post don't forget it was initially written for a friend and may look a bit too personal at some places. But, I don't have the energy to write another version.

I am a coder and I am very very bad at graphics. I have some friends who are good at graphics but very very bad at programming. And, unfortunately, most web frameworks are using templating systems which are mixing code and html. Either the templating system is useful for graphics and weak on programming or it is providing all the power of a functional programming language but not very easy to use for graphic people.

The iPhone is no more a rumor and it is using OS X ! What does it mean ?

One month ago I did not know a lot about logic : just truth tables for some connectives. But, for some time I have been having fun with Haskell and it finally convinced me to use some of my spare time to learn about logic. Of course, you can code in Haskell without knowing a lot about logic, the Curry-Howard isomorphism and all that but it is much more fun to code in Haskell if you know a bit about it.

So, thanks to my Christmas vacations, and the fact that being French I have long vacations :-), I read a few papers about logic : classical, intuitionistic, modal, linear etc... This post is an attempt to summarize what I think I have understood and I hope it may be useful to other newbies too.

I need to have my dose of Haskell everyday :-) But, I have not always access to a computer. So, I have created a widset to allow me to read the blogs from Planet Haskell on my mobile phone. You can get it here : http://www.widsets.com/widgets?publicwidgetid=W1441

Today, I am trying to understand the (->) monad ... not so easy without any example available.