giraj

The construction of the type 'Map<string, Type>' is entirely standard in languages like Agda and Coq (and I bet Idris too). In these languages, Type is itself a type, and can be treated like any other type (like string or int). Nothing clunky about it. (If you're curious, Type is usually referred to as a "universe type" in type theory circles.)

I can't speak for kxyvr, but let me chime in as a mathematician who does formalise my theorems. There's no issue with representing various foundations (e.g. ZFC) on a computer -- for example, that's essentially what Lean/mathlib does, and it's working out great for them. A "problem" with ZFC, however, is that it's very low-level, meaning there's a large distance between the "informal" proofs which mathematicians carry out and communicate, and their corresponding formal proofs in ZFC. Accordingly, for a ZFC-based mathematician to start using proof assistants, they not only have to learn how to use a proof assistant, but also to translate (or expand/elaborate) their math into ZFC.

In other foundations, such as homotopy type theory (which is what the article is about), the distance between "informal" mathematical arguments and their formal counterparts is much shorter. This is why formalisation is widespread in the HoTT-community. Indeed, I believe Voevodsky worked on HoTT in order to have a foundation which was much closer to the mathematical practice in homotopy theory.

That is an extremely uncharitable take. I find that most mathematicians care deeply that their proofs are correct.

Mechanized proofs ensure the correctness of the results they prove. That's useful. Indeed, the point of the article was that Voevodsky sought out proof assistants in order to ensure his math was correct.

As for your other questions: No, formal proofs are not intelligible to the average mathematician. They do not on their own grant insights, but the process of formalising a proof does often yield insights. (I speak from experience.) Not sure what you mean by "better"; they certainly don't replace ("informal") mathematical proofs.

You're not wrong, but most mathematicians aren't working on (or even interested in) foundations. Not saying what you mentioned isn't math (I think it is), but my point still stands.

Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reasons you state for your interest in formalisation don't appeal to most mathematicians.

Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.

The paper argues against those who think that "programming should strive to be more mathematical" through the development and adoption of formal methods. It points out that "more mathematical" does not implicate formal methods, since proofs by mathematicians are informal and their correctness is established by social processes. The author fears that an over-emphasis on formal methods could stifle innovation (in particular, in programming language design).

As a mathematician that works with proof assistants, I largely agree with this thesis. However, I don't think there is any reason to have any such fears associated with formal methods. I think informal proofs, as the exist in both CS and maths, are here to stay. And, on the contrary, I think investigations into formal methods can drive new theory and insight. For example, one could say that the formal system of homotopy type theory (HoTT) is a programming language created in order to reason about highly "coherent" mathematical structures, which HoTT often does very well. In addition, being a formal system, HoTT is well-suited for formal methods -- but even so, many mathematicians still prefer to work informally in this language.

In summary, I think the article makes a valid point, but the motivating fears seems unfounded in retrospect.

Also "I am excited to welcome Linda Yaccarino as the new CEO of Twitter" (current front-page) is tagged 'javascript', which isn't particularly relevant.

They explain that they added an "in-app donations appeal" at the end of 2022, so I imagine that would be it.