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 

[Gershom B]

The other approach, which has been quite successful, by the penn team,
is using hs-to-coq to extract coq from haskell and _then_ verify:
https://github.com/antalsz/hs-to-coq

-g

> --
> You received this message because you are subscribed to the Google Groups "cloud-haskell-developers" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to cloud-haskell-deve...@googlegroups.com.
> To post to this group, send email to cloud-haskel...@googlegroups.com.
> Visit this group at https://groups.google.com/group/cloud-haskell-developers.
> For more options, visit https://groups.google.com/d/optout.

[Tim Watson]

On Mon, 10 Dec 2018, 09:30 Gershom B <gers...@gmail.com wrote:

The other approach, which has been quite successful, by the penn team,
is using hs-to-coq to extract coq from haskell and _then_ verify:
https://github.com/antalsz/hs-to-coq

Thank you! Someone else proposed that off list yesterday too. If we get our layering right, that could definitely be a viable alternative!

I will do some more research. I generally think that https://deepspec.org/ is an awesome idea. :)