4 ms·
These days programming languages actually are used for expressing proofs. They can automatically check them to. For example the Coq theorem proving language. h
by setra 9y ago
These days programming languages actually are used for expressing proofs. They can automatically check them to. For example the Coq theorem proving language.
https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq
Some would argue that writing code IS more fault proof than writing proofs the traditional way.
- contravariant 9y agoI would still trust a mathematical argument I can understand over the output of some automated theorem prover. Of course these aren't mutually exclusive, provided the theorem prover is simple enough to understand.