4 ms·

A core problem is that you don't need super fancy type systems to build robust systems in practice. After a certain threshold, type theory research is exploring

A core problem is that you don't need super fancy type systems to build robust systems in practice. After a certain threshold, type theory research is exploring what's possible in theory, like pure mathematics, not what would be good for practitioners. But one area of large impact for this pure type theory research seems to be the mechanization of mathematics. It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed programming language.

ogogmad 5y ago
> It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed programming language. This is a controversial opinion, and not all mathematicians are enthusiastic about it, whether rightly or wrongly. Michael Harris, for instance, is a major sceptic and opponent. It is still a very interesting idea. And it has had some notable successes already.
- Ericson2314 5y ago
  It's a controversial but good opinion. Mathlib marches on and gets better and better.
- sva_ 5y ago
  I have been wondering why programming is so much more accessible than mathematics to many, considering programming is in some way also a kind of mathematics. I think some of it may have to do with the fact that in programming, one can get immediate and non-judgmental feedback about the correctness of ones solution. In mathematics, it's usually a lot more difficult to verify a solution if you don't already know the answer, so you're dependent on people for it. So perhaps, interactive theorem provers may make mathematics a lot more accessible. But I hope the art of doing it with pen and paper doesn't get lost on us with it.
creata 5y ago
> a proof development system, aka dependently typed programming language. There are proof assistants without dependent types, like Isabelle/HOL.

ogogmad 5y ago

> It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed programming language. This is a controversial opinion, and not all mathematicians are enthusiastic about it, whether rightly or wrongly. Michael Harris, for instance, is a major sceptic and opponent. It is still a very interesting idea. And it has had some notable successes already.

Ericson2314 5y ago
It's a controversial but good opinion. Mathlib marches on and gets better and better.
sva_ 5y ago
I have been wondering why programming is so much more accessible than mathematics to many, considering programming is in some way also a kind of mathematics. I think some of it may have to do with the fact that in programming, one can get immediate and non-judgmental feedback about the correctness of ones solution. In mathematics, it's usually a lot more difficult to verify a solution if you don't already know the answer, so you're dependent on people for it. So perhaps, interactive theorem provers may make mathematics a lot more accessible. But I hope the art of doing it with pen and paper doesn't get lost on us with it.

creata 5y ago

> a proof development system, aka dependently typed programming language. There are proof assistants without dependent types, like Isabelle/HOL.