[ogogmad]

> 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.

[sva_]

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.

[Ericson2314]

It's a controversial but good opinion. Mathlib marches on and gets better and better.