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 restr

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 https://doc.rust-lang.org/beta/nomicon/hrtb.html [2]: http://joeduffyblog.com/2016/02/07/the-error-model/ http://joeduffyblog.com/2016/02/07/the-error-model/