You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Instantly share code, notes, and snippets.
🎯
Focusing
Danial Yekibayev
Refffy
🎯
Focusing
Reverser, programmer.
I enjoy image processing and programming.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The fact that 1 + 1 is equal to 2 is one of those things that is so obvious it may be hard to justify why.
Fortunately mathematicians have devised a way of formalizing arithmetic and subsequently proving that 1 + 1 = 2.
Natural numbers are based on the Peano axioms. They are a set of simple rules that define (along with a formal system) what natural numbers are. So in order to prove 1 + 1 = 2 in Rust we first need a formal system capable of handling logic. The formal system that we'll be using is not some random crate, but Rust's type system itself! We will not have any runtime code, instead the type checker will do all the work for us.
Implementing the Peano axioms
First let's go trough the Peano axioms. The first axiom is that "Zero is a natural number". Basically what it says is that zero exists. In order to express that in the type system, we just write:
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters