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.
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...