[_hardwaregeek]

I highly recommend reading The Little Typer if you want a great book that bridges math and code. It starts out describing Pi, a Lisp with some interesting restrictions (limited recursion, types can have values, etc.). They build up some cool stuff like vectors with the size encoded in the type. All of a sudden, they explain that equality is a type, and any value of said type is a proof! Turns out you can think of many proofs as manipulating data structures to get a value of a certain type.

I wonder how long until we get a somewhat mainstream language with pi types. I know Rust considered adding them. And I recently learned that Rust does allow for quantification over lifetimes^[1]. I could certainly see a language that implements dependently typed arrays. Midori for instance looked into eliding bounds checks with compiler proofs^[2].

[1]: https://doc.rust-lang.org/beta/nomicon/hrtb.html [2]: http://joeduffyblog.com/2016/02/07/the-error-model/

[gergoerdi]

I think at this point, Haskell is the most likely to become the first mainstream PL with Pi types: https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell

[somethingsome]

You should take a look into Lean Theorem Prover (among others) ;)