[plake]

Yeah, "left as an exercise" can mean anything from "this is an undergraduate exercise" to "if you understand both the field and this paper, you could write a different, much longer paper, and we both know this, so let's assume I wrote that one."

It's probably not impossible to build a proof language that makes that kind of thing doable, but I suspect that (a) it would be genuinely difficult to operate it skilfully, much as being a really good developer is difficult, and (b) it would take a huge collective effort on behalf of each research community to prove the foundational results everyone relies on.

Whereas the system we have right now, despite sounding kind of weird to outsiders, mostly works okay? I'm just not sure a switch to formal proofs would be worth the time investment -- or that you could convince the many researchers less interested in tech than myself.

[daxfohl]

I came here to say that maybe it makes things simpler though when everyone speaks the same language, and all proofs are written in the same format.

However then I remembered the new codebase I inherited and OMG it's such a mess because somehow just converting a UI enum to a DB enum is a 25-line function that's repeated over and over everywhere. (Needs to be version-safe for different clients that may have old enum values, needs to create error message in appropriate language, etc, and the callers are in different layers and all have different ways of getting the corresponding info).

So yeah maybe the high-level "I get it, you get it, we all get it, let's just state this an move on" is better.