Does anyone have much experience generating Haskell from Coq?

[Tim Watson]

So far I've been reading
https://www.cs.purdue.edu/homes/bendy/Fiat/FiatByteString.pdf. I'm
interested in the ideas presented in
https://github.com/DistributedComponents/verdi-runtime, which is OCaml
based.

My goal is to provide building blocks for verifying and testing Cloud
Haskell programs. I've been looking at existing frameworks (such as
quickcheck-state-machine/-distributed and hedgehog) for model based
testing, and ways of injecting an application layer scheduler for detecting
race conditions. The final bit of the puzzle is being able to apply formal
methods to verify concurrent/distributed algorithms, and generate some (if
not all) of the required implementation code.

Any pointers to research or prior art would be greatly appreciated.

Cheers,
Tim Watson
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20181208/b266eb64/attachment.html>