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?