I have found myself experience a growing fascination with the Rust type system. One manifestation of this fascination, in combination with another long-term interest of mine: formal mathematical systems and models, entailed that I be doomed to construct the natural numbers in the language of said type system. Prominent applications of these kinds of type systems include not just specifying how abstract data is represented in machine code ("is this sequence of bits a number? a string? what?"), but also eliminating a wide range of erroneous run-time behaviors via compile-time guarantees. This would mean that numbers, operations on them, and their properties can exist at compile-time, and we can prove things about them without ever running the associated program. The Rust compiler becomes a proof-checker.

I willingly yielded to that inclination, and this article will try to walk you through a process similar to mine.

ecsolticia

@ecsolticia.bsky.social

I got a bit sidetracked from my current project into further exploring the capabilities of Rust's type system. Peano axioms were way too fun play around with. I got to the point of having a proof that 5 + 5 = 10. (Compilation here proves the validity of the statement within what I constructed)

Sep 1, 2025, 6:10 PM

4

The source code for the project, which also includes more operations and properties than explored here, can be found on Codeberg and Tangled.

The Peano Axioms

The Peano axioms are a set of propositions that, if taken to be true together, describe the natural numbers (0, 1, 2, 3, ...). While some mathematicians and enthusiasts may not consider 0 to be a natural number, for the purposes of this post, 0 is also considered a natural number.

Now, what are the Peano axioms?

First, let's take two symbols for the "language" that I will use to express the Peano axioms: "0" and "++". Here, "0" represents exactly what you might think it does, but instead of taking its meaning for granted, the Peano axioms give it that meaning. In this case, "++" simply represents the successor operator as seen in many programming languages, where 1++ is 2, 54++ is 55, etc. Similar to the case for "0", the Peano axioms do not take this meaning for granted but define it in terms of more "fundamental" properties. This is crucial in abstracting the domain of discourse further and allowing us to reason about a wider range of properties, without going down so far that we are effectively talking about everything.

With that setup, let's jump into the axioms.

The most basic one might seem ridiculously trivial.

1. 0 is a natural number.

Before you question why we are even doing this, remember that the Rust compiler does not know that we wish to associate something we might consider "0" with something it and many other similar things can share, which we might call the fact of being natural numbers. We need to ground what it "knows" in these basic, fundamental, seemingly trivial statements.

2. If N is a natural number, then N++ is a natural number.

At this point, our axioms still do not allow us to fully comprehend what "++" entails. However, it at least provides us the information that whatever "N++" is for any N, it has to be a natural number, whether N itself or something else. This also immediately means that 0++ is a natural number. It might be tempting to assume that this is all we need, but note that even if we let 0 = 0++, we have no contradiction within our present assumptions. Clearly, we don't want 0 = 1! (factorial pun intended)

| 3. For natural numbers N and M, if N++ = M++, then N = M.

Does this prevent us from the 0 = 0++ scenario? Almost! If 0 = 0++, then surely there can be some X such that X++ = 0. We want to eliminate this X, because we are veering off into negative numbers. BUT, our current set of axioms does not lead to any contradiction in the presence of that fact. We need more.

Note that it also wouldn't rule out something like 0++ = (0++)++ yet, which 0 = 0++, which takes us back to the X = 0 scenario. It is left as an exercise to the reader to extrapolate this further (I wanted to do the "it is left as an exercise to the reader" thing so bad!).

4. If N is a natural number, then N++ = 0 is always false.

Finally, there can't be any abomination of an X such that X++ = 0. Finally, we can rule out the 0 = 0++ case, the (0++)++ = (((0++)++)++)++ case, or the (((0++)++)++)++ = (((((0++)++)++)++)++)++ case.

Surely, we are done!

5. The axiom of induction

Huh?

We are only able to obtain larger numbers by successively applying the successor operator ++. It would not be possible, even in principle, to prove that all powers of 2 are even, just through this tedious approach. We need to get clever... kind of. Luckily, mathematicians are already clever. They know how to handle this.

Behold, the axiom of induction. It goes like this:

Let K be some set.

Suppose that

- 0 is in K

- If a natural X is in K, then X++ is in K.

Then it follows that all natural numbers are in K.

The justification for this axiom itself is a deep rabbit hole. Not going there for this post! BUT, let's satisfy ourselves with an intuitive explanation:

Let's say that IF a natural X is in set K, then X++ is in set K.

What we get? ... crickets chirps.. okay, we only assumed a conditional. For something to actually happen, we need something that satisfies the condition. For that, we need a natural in K.

Let's just say that 0 is in K! What we get now? Too much! Since 0 is in K, and a natural X being in K means that X++ is in K, surely, 0++ is in K! Similarly, (0++)++ is in K, ((0++)++)++ is in K, (((0++)++)++)++ is in K, and it keeps going ad infinitum!

This axiom will be particularly important as we will define most properties in the Rust type system using the inductive approach.

The Approach

Formally, the Peano axioms make home in a system of logic. Here, notions of truth values (whether something is true or false, or the extent of truth as in fuzzy logic, etc), operations such as AND and NOT that communicate their relationships, and quantifiers like "there exists" or "for all" hold meaning.

The boolean operations in Rust such as && and || are generally evaluated at run-time, and operate on values than types. Similarly, what would be a "for all" quantifier in Rust, at compile-time? You may define a finite collection and have a loop verify certain properties, but this is also clearly a run-time process.

Instead, we can use structs to define new types, such as numbers, and traits and associated types to represent properties and relationships. Importantly, we can use generics, trait bounds and the where keyword to specify conditions for implementing certain traits for certain types, which corresponds to conditionally assigning properties and relations to numbers.

Let's Go!

Laying Out The Axioms

We'll have each number be a distinct type. Let's first define the number zero according to the first axiom, which says that 0 is a natural number.

As per our approach, the property of 0 being a natural number would require a trait, which we can implement on certain types to indicate that they represent natural numbers.

pub trait Nat {}

As for 0, there are a few different ways we could go about this. We could create a new empty struct such as struct _0 {}, alias the unit type like type _0 = (), or do something else.

Let's go with the latter approach:

pub type _0 = ();

Now, we have a type alias for representing 0, but the compiler can't yet tell that _0 is a natural number. Let's do

impl Nat for _0 {}

There we go! First axiom done.

The next axiom states that if N is a natural, then so is N++. For this, we need a way to represent N++ given N at compile-time. We can use generics and structs:

pub struct Succ<T>(T);

Now, given any type N which implements Nat (representing natural number N) we can represent N++ as Succ<N>. The struct holds a 1-tuple containing T because in Rust, every generic to a struct must be used at least once, but we are only using it to mark different types. It is more idiomatic to use std::marker::PhantomData to hold the generic parameter to avoid additional memory from being used for it at run-time, but we are not interested in running the program.

However, while we can easily take Succ<_0> right away, it will not be a natural number just yet. This isn't given to us for free, we have to make the compiler apply the equivalent of induction (the fifth axiom) for us.

impl<T: Nat> Nat for Succ<T> {}

Given any T that implements Nat, this block will implement Nat for Succ<T>.

Note that if N and M implement Nat, and Succ<N> and Succ<M> happen to be the same types, N and M must be the same types. This is the third Peano axiom we explored, and it IS given to us for free.

Similarly, if N implements Nat, then Succ<N> surely can't be _0 by type! If type equivalence is the only property we use here to judge equality between represented naturals, then clearly, this means we are also given the fourth axiom for free.

So far, this is what we have:

pub trait Nat {}
pub struct Succ<T>(T);

pub type _0 = ();
impl Nat for _0 {}
impl<T: Nat> Nat for Succ<T> {}

These five lines constitute the whole foundation for what we will build in the next sections!

As an aside, if you are wondering why the items here such as Nat and _0 are pub, it is because I have them in my src/lib.rs than src/main.rs. I only kept tests of behavior in src/main.rs. If you do not want that separation, you could remove the pub keywords.

Count to Ten

So far, the only concrete number we constructed is 0. Let's count to ten!

pub type _1 = Succ<_0>;
pub type _2 = Succ<_1>;
pub type _3 = Succ<_2>;
pub type _4 = Succ<_3>;
pub type _5 = Succ<_4>;
pub type _6 = Succ<_5>;
pub type _7 = Succ<_6>;
pub type _8 = Succ<_7>;
pub type _9 = Succ<_8>;
pub type _10 = Succ<_9>;

Learning to Add

Sure, we can now count up by repeatedly applying succession. But can we add numbers?

Well, addition in the domain of the natural numbers is just repeated succession, the same way multiplication is repeated addition, and exponentiation is repeated multiplication. We establish a base case (the case where we take 0 and establish that it has a property), the inductive hypothesis (that if N satisfies that property, so does N++), and use the axiom of induction to prove that it applies to all naturals.

We will also represent the property of some number being "addable" to another by a trait, as per the "approach" section. However, it will also have an associated type implementing Nat, which will represent the result of addition. Here's how this looks:

pub trait Add<RHS: Nat> {
    type Sum: Nat;
}

If Add<N> is implemented for M, it means that N can be added to M. We can take the sum with <M as Add<N>>::Sum.

Let's implement the base case: any number + 0 = that number.

impl<T: Nat> Add<_0> for T {
    type Sum = T;
}

Given any T that implements Nat, this block will implement Add<_0> for T with Sum set to T itself. This is the same as stating that given any natural number N, N + 0 = N.

To define addition based on succession, let's say that if A and B are naturals, then

A + (B++) = (A + B)++

Why do we even need this? Well, this allows us to define addition for all naturals inductively (which corresponds to implementing Add for all Nat-implementing types inductively). We can take any natural A, and if A + B is defined, we can take A + (B++) = (A + B)++, the R.H.S. of which is also defined.

Applying this in Rust, we get:

impl<A: Nat, B: Nat> Add<Succ<B>> for A
where
    A: Add<B>
{
    type Sum = Succ< < A as Add<B> >::Sum >;
}

What does this mean? Well, the take two generic parameters A and B implementing Nat, and if A implements Add<B> (as specified by the where keyword), the the compiler implements Add<Succ<B>> for A for us. Here, the where keyword is doing a job similar to that of an if statement or a scope quantifier in a system of formal logic. It restricts A to be only the kind of Nat-implementing type which can add B to itself to give us <A as Add<B>>::Sum (A + B). From this, we make it possible for A to add B++ (implement Add<Succ<B>> for A), and specify that said sum must be whatever we set the Sum type inside of it to. In this case, Sum can be thought of as being Succ<X> (X++) where X is <A as Add<B>>::Sum (A + B). Thus, it represents (A + B)++. Combining all this, this step inductively equates A + (B++) to (A + B)++.

This is in fact all we need to define addition!

If we take something like <_5 as Add<_0>>::Sum, the compiler can directly match it to the base case, and give us _5 back.

If we instead take <_5 as Add<_1>>::Sum, it is matched to the more general impl block which represents the inductive hypothesis and induction. The compiler matches _1 with the Succ<B> in Add<Succ<B>>, and requires that _5 implements Add<B> due to our usage of where. Given so, it finds that Succ<_0> is _1, and _5 indeed already implements Add<_0> as per the base case. Consequently, Succ< < A as Add<B> >::Sum > just becomes Succ<A>. In this case, we get our expected _6.

In general, given any N which implements Nat, taking <N as Add<M>>::Sum just means "applying" Succ to N exactly as many times as the number that M represents. This is how addition here is repeated succession.

Equality and Identity: He is Mi and I am Yu

So far, we have constructed a system that can "count" and add numbers. That's nice! However, how can we check that it adds numbers correctly, other than trying to prove that it does from first principles?

Well, we need a notion of equality for that. As previously stated, if A and B stand for types or a type implementing Nat, we'll consider them "equal" if and only if A and B stand for the exact same type.

Implementing this is simple. We can define a type with a generic parameter to compare a type with, and implement it only for the type in the generic parameter:

pub trait Eq<A: Nat> {
    fn equal() -> () {}
}

// Implement Eq<A> for any A implementing Nat
impl<A: Nat> Eq<A> for A {}

The trait has an equal function, which we can call to check if Eq<A> is implemented for some type B. If it is not implemented, which could only be if A and B are distinct types, then the compiler will scream at us for trying to call a non-existent function. Similar to addition, we can call this function as <A as Eq<B>>::equal().

Reality Check: Does our addition mechanism work?

Let's test it out!

fn five_plus_five_is_ten() {
    type Claimed10 = <_5 as Add<_5>>::Sum;

    type Verified10 = _10;

    <Claimed10 as Eq<Verified10>>::equal();
}

If you're following along and kept the core logic intact, this program should compile just fine!

Let's test a case where it absolutely should not compile. We know that 2 + 3 shouldn't be 6.

fn two_plus_three_is_six() {
    type Claimed6 = <_2 as Add<_3>>::Sum;

    type Verified6 = _6;

    <Claimed6 as Eq<Verified6>>::equal();
}

If you try to compile THIS, you might get something like:

error[E0277]: the trait bound `Succ<Succ<Succ<Succ<Succ<()>>>>>: Eq<Succ<Succ<Succ<Succ<Succ<Succ<()>>>>>>>` is not satisfied
  --> src/main.rs:54:6
   |
54 |     <Claimed6 as Eq<Verified6>>::equal();
   |      ^^^^^^^^ the trait `Eq<Succ<Succ<Succ<Succ<Succ<Succ<()>>>>>>>` is not implemented for `Succ<Succ<Succ<Succ<Succ<()>>>>>`

For more information about this error, try `rustc --explain E0277`.
error: could not compile `rspeano_follow` (bin "rspeano_follow") due to 1 previous error

This is simply saying that Claimed6, which we really expect to be _5, doesn't implement Eq<_6>, which is expected!

On the other hand, you can check that Claimed6 is indeed _5 through a successful compilation of <Claimed6 as Eq<_5>>::equal().

Learning to Multiply

Okay, cool, we can add now, and correctly. Toddler stuff. Now, let's see how we do the 10 × 2 = 20 stuff. As mentioned previously, multiplication of the naturals can be defined based on addition. Specifically, as repeated addition. It extends addition the same way addition extends succession. Let's jump into it!

pub trait Times<RHS: Nat> {
    type Prod: Nat;
}

Similar to Add, if Times<X> is implemented for a type N implementing Nat, then N can multiply X. Again, we can take the product of N and X as <N as Times<X>>::Prod.

Let's implement the base case. We know that any N multiplied by 0 is 0.

impl<N: Nat> Times<_0> for N {
    type Prod = _0;
}

This is very much analogous to the base case trait implementation for Add.

To define multiplication based on addition, if A and B are natural numbers, then let's say that

A × (B++) = (A × B) + A

This, indeed, is also analogous to our inductive statement for addition. Here, addition by A is analogous to succession in the inductive statement for addition itself. A × 0 is already covered by the base case, and the rest is handled by the inductive statement!

impl<A: Nat, B: Nat> Times<Succ<B>> for A
where
    A: Times<B>,
    <A as Times<B>>::Prod: Add<A>
{
    type Prod = <
                <A as Times<B>>::Prod
                as Add<A>
                >::Sum;
}

It might seem as though this impl block escalated in complexity, but let's walk through it step by step.

The first line by itself might be familiar, it takes two natural numbers A and B, and suggests that it will specify how to multiply A by B++.

The constraints specified using the where keyword are like this:

• A: Times<B> means that A must be able to multiply B, since we need this to be able to take (A × B).

• <A as Times<B>>::Prod: Add<A> means that the product of A and B (<A as Time<B>>::Prod) must be able to add A. This is so that after we get (A × B), we can also take (A × B) + A from it.

Finally, we set Prod to said type representing (A × B) + A.

Again, this is all that was needed to define multiplication! It resolves non-base cases similar to how addition does. Let's use our equality trait again to see if it works the way we expect!

Reality Check: Does <A as Times<B>>::Prod Respect the Times Table?

Again, we test it out similar to how we tested addition.

One Times One

fn one_times_one() {
    type Claimed1 = <_1 as Times<_1>>::Prod;

    type Verified1 = _1;

    <Claimed1 as Eq<Verified1>>::equal();
}

Result: Expected - Compiles.

Zero Times Ten

fn zero_times_ten() {
    type Claimed0 = <_0 as Times<_10>>::Prod;

    type Verified0 = _0;

    <Claimed0 as Eq<Verified0>>::equal();
}

Result: Expected - Compiles.

Five Times Two = Seven Plus Three

fn five_times_two_is_seven_plus_three() {
    type Prod = <_5 as Times<_2>>::Prod;

    type Sum = <_7 as Add<_3>>::Sum;

    <Sum as Eq<Prod>>::equal();
}

Result: Expected - Compiles.

False: Ten Times Ten is Five

fn ten_times_ten_is_five() {
    type Claimed5 = <_10 as Times<_10>>::Prod;

    type Verified5 = _5;

    <Claimed5 as Eq<Verified5>>::equal();
}

Result: Expected - Fails to compile.

It yields the following (expected) error:

error[E0277]: the trait bound `Succ<Succ<Succ<Succ<...>>>>: Eq<...>` is not satisfied
  --> src/main.rs:97:6
   |
97 |     <Claimed5 as Eq<Verified5>>::equal();
   |      ^^^^^^^^ unsatisfied trait bound
   |
   = help: the trait `Eq<Succ<Succ<Succ<Succ<Succ<()>>>>>>` is not implemented for `Succ<Succ<Succ<Succ<Succ<...>>>>>`

I could go on, but if you are following along, try changing random numbers here and there (e.g. changing some _4 to _5) and see what you get!

Exponentation

Not so much of toddler stuff anymore, but still kid stuff. We can do this!

This will work very similar to multiplication. If you have been following along and are up for it, maybe you can try to construct this yourself!

To start, let's do

pub trait Exp<E: Nat> {
    type Pow: Nat;
}

The base case, again, is rather simple:

impl<A: Nat> Exp<_0> for A {
    type Pow = _1;
}

Now, similar to how we based addition on repeated succession, multiplication on repeated addition, we can now base exponentiation on repeated multiplication:

A ^ (B++) = A ^ B * A

Given this, we can implement the exponentiation trait on the naturals as follows

impl<A: Nat, B: Nat> Exp<Succ<B>> for A
where
    A: Exp<B>,
    <A as Exp<B>>::Pow: Times<B>
{
    type Pow = <
               <A as Exp<B>>::Pow
               as Times<A>
               >::Prod;
}

Note that this is very similar to our trait impl block for multiplication. Given two natural numbers A and B where A ^ B is defined, and (A ^ B) * A is defined, we define (A ^ (B++)) as the latter.

Similar to addition and multiplication, again, we can take base A raised to B as <A as Exp<B>>::Pow.

With all these rules set, we can now prove and disprove a wider array of arithmetic equations!

Proofs Proofs Proofs

So far, we have constructed a system of arithmetic over the natural numbers with succession, addition, multiplication, and exponentiation being its "first-class citizens". Given these operations, we can start to prove some more involved (still basic) arithmetic facts, and disprove some false statements, using just the rust compiler!

3^2 + 4^2 = 5^2

A classic, lovely application of the Pythagorean theorem!

fn pytha_triple() {
    type A = <_3 as Exp<_2>>::Pow;
    type B = <_4 as Exp<_2>>::Pow;
    type R = <_5 as Exp<_2>>::Pow;

    type LHS = <A as Add<B>>::Sum;

    <R as Eq<LHS>>::equal();
}

Result: Expected - Compiles.

3 × 2^2 + 9 = (5 × 4)++

An equation that includes all four of the operations we defined.

fn all_four() {
    type A = <
             <_3 as Times< <_2 as Exp<_2>>::Pow >>::Prod
             as Add<_9>
             >::Sum;

    type B = Succ<
             <_5 as Times<_4>>::Prod
             >;

    <A as Eq<B>>::equal();
}

Result: Expected - Compiles.

False: 1^(10 * 10) = 10

fn one_raised_to_100_is_ten() {
    type LHS = <
               _1 as Exp<
                        <_10 as Times<_10>>::Prod
                        >
               >::Pow;
    type RHS = _10;

    <LHS as Eq<RHS>>::equal();
}

Result: Expected - Fails to compile.

It yields the following (expected) error:

error[E0277]: the trait bound `Succ<()>: Eq<Succ<Succ<Succ<...>>>>` is not satisfied
   --> src/main.rs:110:6
    |
110 |     <LHS as Eq<RHS>>::equal();
    |      ^^^ unsatisfied trait bound
    |
    = help: the trait `Eq<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<()>>>>>>>>>>>` is not implemented for `Succ<()>`

False: 2^4 = 5^3 + 6 * 5 + 3

fn another_false_equation() {
    type LHS = <_2 as Exp<_4>>::Pow;

    type A = <_5 as Exp<_3>>::Pow;
    type B = <_6 as Times<_5>>::Prod;
    type RHS1 = <A as Add<B>>::Sum;
    type RHS = <RHS1 as Add<_3>>::Sum;

    <LHS as Eq<RHS>>::equal();
}

Result: Expected - Fails to compile.

It yields the following (expected) error:

error[E0277]: the trait bound `Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<...>>>>>>>>>>: Eq<...>` is not satisfied
   --> src/main.rs:110:6
    |
110 |     <LHS as Eq<RHS>>::equal();
    |      ^^^ unsatisfied trait bound
    |
    = help: the trait `Eq<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<()>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>` is not implemented for `Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<()>>>>>>>>>>>>>>>>`

Again, if you've followed along, you can try your own examples!

A Caveat: Recursion Limits and Large Numbers

If you use sufficiently large numbers such as <_2 as Exp<_10>>::Pow, checking its equality with something else might mean hitting a recursion limit. Given that the way we constructed the naturals inevitably requires recursive unwinding, the most direct way to circumvent these errors would be to increase the recursion_limit attribute. The repository pertaining to this post keeps the limit at the rustc default of 128 and avoids large numbers.

Wrapping Up

We started off with just a simple unit type, said that it represents zero, and inductively defined successive types representing successive natural numbers as per the Peano the axioms. Using the notion of succession, we defined addition, using which we defined multiplication, from which we got exponentiation. We got all of this with the foundation of a mere 5 lines, as represented near the start of the "Let's Go!" section:

pub trait Nat {}
pub struct Succ<T>(T);

pub type _0 = ();
impl Nat for _0 {}
impl<T: Nat> Nat for Succ<T> {}

My repository (Codeberg | Tangled) for this project also implements:

• Parity properties: check whether a natural is odd or even at compile-time.

• Inequalities: The "less than or equal to" and "greater than or equal to" relations.

If you've been following along and feel confident enough, you could try defining these yourself! Perhaps even add your own. If you wish to check my own definitions, the repository is just there.