Using "and" like this is a common shorthand for "the sum of n and m is...". The shorthand is a bit antiquated now, but you can find it in a lot of arithmetic books (and song lyrics).
It's quite cool that you can use type systems in "regular" languages to do such things.
Notice though, that this system is not powerful enough to prove all the facts about the natural numbers. For example, the author states that this system has the property that there is no number smaller than zero. This is true, at least if we define "smaller than" transitively via the successor function (/ type constructor). However, it's still entirely possible to define a "struct NegativeOne();" and define addition so that -1+1=0, so you can't prove that there is no number such that when you add to it a nonzero number, you get zero. More generally, this system doesn't actually formally define the natural numbers, it just constructs a finite number of them (which is fine, the article didn't claim otherwise). I don't know if Rust's type system is powerful enough to construct the natural numbers in some "natural" way (it's mentioned that the type system is Turing complete, but that doesn't technically guarantee that such an encoding would be practical to use), you'd need some way of writing an inductive type definition where Zero is a Nat and Succ<N> is a Nat iff N is s Nat.
I think that this is correct and a consequence of Gödel's incompleteness theorems, although my knowledge about this is quite sketchy.
What I was referring to more (and should have clarified better) was that there are models of arithmetic that can characterise the natural numbers uniquely (up to isomorphism) - translated to type theory, it is possible in languages like Coq and Lean to fully define what a natural number is without including any extra objects - even if you won't be able to prove all theorems about them. Notably, though, first order theories are not sufficient to define the natural numbers, for every set of first-order axioms about the natural numbers, there are "non-standard models" that can look quite weird. You need second-order logic or something equivalent in power to prevent that (the difficult axiom here is the axiom of induction which needs to be able to quantify over predicates).
22 comments
[ 3.4 ms ] story [ 63.9 ms ] threadSee https://news.ycombinator.com/item?id=14944003 for another submission that had this issue.
More interestingly, 2+2=4: http://us.metamath.org/mpegif/2p2e4.html
(also have a look at the trivia: http://us.metamath.org/mpeuni/mmset.html#trivia !)
Notice though, that this system is not powerful enough to prove all the facts about the natural numbers. For example, the author states that this system has the property that there is no number smaller than zero. This is true, at least if we define "smaller than" transitively via the successor function (/ type constructor). However, it's still entirely possible to define a "struct NegativeOne();" and define addition so that -1+1=0, so you can't prove that there is no number such that when you add to it a nonzero number, you get zero. More generally, this system doesn't actually formally define the natural numbers, it just constructs a finite number of them (which is fine, the article didn't claim otherwise). I don't know if Rust's type system is powerful enough to construct the natural numbers in some "natural" way (it's mentioned that the type system is Turing complete, but that doesn't technically guarantee that such an encoding would be practical to use), you'd need some way of writing an inductive type definition where Zero is a Nat and Succ<N> is a Nat iff N is s Nat.
You can do such things in theorem provers, here's a tutorial on how to do it in Lean: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
What I was referring to more (and should have clarified better) was that there are models of arithmetic that can characterise the natural numbers uniquely (up to isomorphism) - translated to type theory, it is possible in languages like Coq and Lean to fully define what a natural number is without including any extra objects - even if you won't be able to prove all theorems about them. Notably, though, first order theories are not sufficient to define the natural numbers, for every set of first-order axioms about the natural numbers, there are "non-standard models" that can look quite weird. You need second-order logic or something equivalent in power to prevent that (the difficult axiom here is the axiom of induction which needs to be able to quantify over predicates).