Very interesting, and I'd never heard of Curry-Howard correspondence. I've also always wondered how dependent types worked conceptually (as in, what's going on

Very interesting, and I'd never heard of Curry-Howard correspondence. I've also always wondered how dependent types worked conceptually (as in, what's going on there, what are we proving, etc). Thanks for the insights and the links!