4 ms·
Obviously I mean an ML-like type system with automatic inference. Otherwise it is just general logic, and you definitely don't need types for that. And Curry-H
by auggierose 3y ago
Obviously I mean an ML-like type system with automatic inference. Otherwise it is just general logic, and you definitely don't need types for that.
And Curry-Howard is the most overrated isomorphism in history. It may make computer scientists head explode, but mathematicians can live without it.
And yes, I know that Lean is based on it, and Tao is using it, and he just doesn't know better. Sorry.
- layer8 3y agoType inference is largely orthogonal to the question. The point is, any formal proof you could do outside a type system you can also do within a type system, so yes the right type system would help you avoid such bugs.
- auggierose 3y agoNo, that's not the point. There is no point to a general type system without automatic type inference. Because otherwise, it's just a kind of cumbersome and cobbled together logic.