Coq.io

Voice your Coq.

Coq.io is a library to write Coq programs with IO and concurrency. You code, you certify and you compile to a runnable OCaml program with verified IO.

Try

Setup OPAM for Coq and run:

opam install coq-io-hello-world
helloWorld
==> Hello world!

Then go to Getting started.