Coq is an interactive theorem prover. It allows the express…
Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification
Replies
@14
https://twetch.app/t/993763d901ad0cf4948459259354a31c877528d0b42132d5390236406b96303b
You should check out the work of Alexander Stepanov.
will do
I like it but it can all be done in c++ (I'm still working out how)