3 ms·
I'm a fan of both sides of the Coq and Isabelle/HOL activities. I'm keeping an eye on CertiCoq. Right now, though, Isabelle/HOL seems to be ahead with work like
by nickpsecurity 9y ago
I'm a fan of both sides of the Coq and Isabelle/HOL activities. I'm keeping an eye on CertiCoq. Right now, though, Isabelle/HOL seems to be ahead with work like Myreen and Davis's in terms of verified stacks:
https://www.cl.cam.ac.uk/~mom22/ https://www.cl.cam.ac.uk/~mom22/
This data structure refinement with one version getting automated to a large degree:
https://www21.in.tum.de/~lammich/pub/cpp2016_impds.pdf https://www21.in.tum.de/~lammich/pub/cpp2016_impds.pdf
Thanks to DeepSpec, Coq might exceed that in some ways:
https://deepspec.org/main https://deepspec.org/main
Note that a lot of work around Coq goes through CompCert which is proprietary software with restrictions on how it's used if one doesn't pay. The Isabelle/HOL alternatives like Simpl/C and CakeML are free software. Then, outside those two, we got a bunch of work being done in Maude (esp K Framework) with one an executable, formal semantics for C done like a compiler:
https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics