Junglefowl runs Peano arithmetic on Rust types, verified at compile time.
Here's our Peano encoding:
0 <--> ()
1 <--> ((), ())
2 <--> ((), ((), ()))
3 <--> ((), ((), ((), ())))
Note that, thanks to a clever abuse of Rust's syntax, these are both types and values.
Next, there's a macro so you can forget what you just read:
rust
peano!(0);
--> ()
peano!(42);
--> ((), ((), ((), ((), ((), ((), ((), ((), ((), ...)))))))))
Note that this macro expands to a type, so you would use it like this:
rust
let x: peano!(42) = todo!();
instead of like this:
rust
let x = peano!(42); // bad!
And next, there's a hell of a lot of other stuff, but instead of explaining it all, watch this compile:
rust
static_assert_eq!(peano!(39), sub!(peano!(42), peano!(3)));
expands to
```rust
enum False {} // uninstantiable type
// this part vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv evaluates to zero when the two sides are equal
const : [False; (peano!(39) != sub!(peano!(42), peano!(3))) as usize] = [];
// ... which makes the list length zero, which matches the right-hand side (and couldn't be nonzero since its members are uninstantiable)
// learned the list length trick from the static_assertions crate, so all credit there!
Expanding the interesting part above (and inverting so `!=` becomes `==`):
rust
peano!(39) == < peano!(42) as peano::Sub< peano!(3) >>::Difference;
peano!(39) == <((), ((), ((), peano!(39)))) as peano::Sub<((), ((), ((), ())))>::Difference;
Here's the definition of `peano::Sub`, pretty representative for most operations in this crate:
rust
pub trait Sub
Begin reduction!
rust
peano!(39) == <((), ((), ((), peano!(39)))) as peano::Sub<((), ((), ((), ())))>::Difference;
peano!(39) == < ((), ((), peano!(39))) as peano::Sub< ((), ((), ())) >::Difference;
peano!(39) == < ((), peano!(39)) as peano::Sub< ((), ()) >::Difference;
peano!(39) == < peano!(39) as peano::Sub< () >::Difference;
peano!(39) == peano!(39) ;
```
_et voila!
A certain well-known theorem prover is named after the French word for ~~cock~~ rooster (coq), so I Googled "rooster" and found (to my amazement!) that they belong to the junglefowl species. This name sounded suitably cool.