Is there any material on practical programming in Coq?

Question

I just finished reading Coq in a Hurry, which is a very good tutorial I found online. I got very exited about Coq.

Is there any material on practical programming in Coq? Like printing the result of a function, String output, reading/writing to a file, etc.? I know it is possible to use code extraction to generate haskell or ocaml code, but I cannot find good examples or a tutorial.

Further, is there something similar to the Agda FFI in Coq?

Answer 1

Adam Chlipala explains at some length, including Generic Programming (for Coq users), which you may find helpful.

Answer 2

There is no Foreign Function Interface in Coq. Calling an external function does not make sense as foreign code cannot be verified. You cannot even prove termination to Coq. I asked pretty much the same question to Pierre Letouzey during a 2010 summer school on Coq and he replied that the idea is to write the tricky algorithms with Coq and extract a verified implementation in Ocaml or Haskell (he was working on the latter then) to integrate in a "real program".

You can find something about how to extract code in the manual.

Answer 3

There is the Petit guide de survie en Coq ("small Coq survival guide") but as far as I know there is only a french version. However, it seems to be simple enough to get a understandable result with an automatic translation tool (here with Google).