I can understand where this is coming from, but as a PhD in Pure Math who is now a programmer, I think it is badly misleading. Many people here will speak eloquently about how wonderful proof assistants are, and how lamentable it is that modern mathematicians don't use them, but then it usually transpires that they themselves are not mathematicians, and really don't have a clue about just how free form mathematics is when practised at the highest levels.

I'm sure computer assisted and computer annotated proofs will advance marvellously over the coming decades, but it seems incomprehensible to me that modern research mathematics could be done within that framework.

It would be interesting to be proved wrong, but it seems that the skills required to use the current level of proof assistants would be much like asking modern web programmers to use front panel toggle switches. Toy programs would be onerous, but possible. Anything with any real content would require specialists in the assistant language. Suddenly you're asking mathematicians to be programmers as well, albeit in a specialised language.

From what I've seen, it's still like programming in assembler. Or worse. I've seen and have had some training in proof-assistant languages, and at their current status it just seems hopeless for real work.

I look forward to seeing how it will develop over the coming decades, although I doubt I will still be a working programmer, or mathematician, by the time it becomes possible to express mathematics at the highest level in proof assistant languages.

Despite disagreeing with it, here is the text:

================================================================

Imagine if I asked you to learn a programing language and a culture of practices
where:

- All the variables were a single letter, pathologically so, and that programmers
enjoyed using foreign alphabets, glyph variation and fonts to disambiguate their
code from meaningless gibberish.

- None of the functions were documented independently, and instead the API
documentation consisted of circular references to other pieces of similar
code, often with the same names overloaded into multiple meanings, often
impossible to Google.

- None of the sample code could be run on a typical computer, in fact, most
of it was pseudo-code lacking a clear definition of input and output, or
even the environment and domain in which it is typically expected to be run.

- Expressive code in this language was impossible to write in a typical text
editor or word processor, and transcribing code from paper back into something
useful was an error-prone process.

- Papers describing novel ideas in the field were incomprehensible by default,
so that the world's most established experts on the subject would need years
to decide whether a particularly cutting-edge program is meaningful or in
fact insane gibberish.

- These experts not only see nothing wrong with this picture, but in fact,
revel in symbolic obscurity and ego-driven naming, dismissing sincere
attempts at fixing these deep seated problems as meaningless taste arguments
or pointless pop culture entertainment.

If you were an experienced programmer. you would rightly call me insane.

If you were a mathematician, it would be a day ending in y.

================================================================