1sNJWUrAYfdxAKN1zGq3t9hwyR6ynQwas (2022) ·
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
1sNJWUrAYfdxAKN1zGq3t9hwyR6ynQwas (2022) ·
@14
1NUNwLXhkvD6uUDRyvbnQZQy5D1ABP2iDE (7453) ·
https://twetch.app/t/993763d901ad0cf4948459259354a31c877528d0b42132d5390236406b96303b
1Jyk8t6Akn3Hem6bTeb4327c9GrYqArPc3 (1487) ·
You should check out the work of Alexander Stepanov.
1sNJWUrAYfdxAKN1zGq3t9hwyR6ynQwas (2022) ·
will do
1Abd9yJS6mrzMmj1Ni6kjQB9GqtyaNujrm (3375) ·
I like it but it can all be done in c++ (I'm still working out how)