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 On Sat, Dec 8, 2018 at 7:05 AM Tim Watson <watson.timo...@gmail.com> wrote: > > 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 > > -- > 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-developers+unsubscr...@googlegroups.com. > To post to this group, send email to > cloud-haskell-develop...@googlegroups.com. > Visit this group at https://groups.google.com/group/cloud-haskell-developers. > For more options, visit https://groups.google.com/d/optout. _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
