5 ms·
How current proof assistants work is using the Curry-Howard correspondence, [1] the gist of it is that all of first order logic can be encoded into a type. All
by davemp 8y ago
How current proof assistants work is using the Curry-Howard correspondence, [1] the gist of it is that all of first order logic can be encoded into a type. All one must do is write an expression that type checks to what one is trying to prove. That turns out to be fairly hard for reasonably complex proofs.
[1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- Twisol 8y agoTo be only a little more precise, every proposition becomes a type of its own. The AND operator forms product types, the OR operator forms sum types, IMPLIES forms a function type... The proof of a theorem turns into an inhabitant of the theorem's type.