4 ms·
Are 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.prince
by unboxed_type 8y ago
Are 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.