3 ms·
There's a new extractor that can output C from Coq. There's also multiple compilers for each language you can extract to. My solution was to do diverse compilat
by nickpsecurity 8y ago
There's a new extractor that can output C from Coq. There's also multiple compilers for each language you can extract to. My solution was to do diverse compilation where multiple compilers, OS's, and ISA's compiled the compiler. Then you just run it through itself on each one. Use end result that most agree on.
- unboxed_type 8y agoAre you talking about CertiCoq project? It is not ready yet and not clear when will be. [1] https://www.cs.princeton.edu/~appel/certicoq/ https://www.cs.princeton.edu/~appel/certicoq/
- nickpsecurity 8y agoTalking about this: https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.pdf https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114.... They extract from Coq to C. Like in my Brute-Force Assurance concept, that would let us confirm and supplement the formal verification by hitting the C output with every V&V tool for C programs that we have on hand.