[webmaven]

> That is just an example of bad exposition in my opinion [and] a perfect example of why arguments like "does this proof make coq happy" totally misses the point..

In theory, some kind of checker could validate the semantics of a paper to just tell you whether the arguments made are complete. Not whether there is a correct formal proof, just pointing out any obscured leaps of faith[0]. A rough analogue to test suite coverage for code (which is also not any sort of guarantee of correctness, just basic reassurance that all (or most of) the code is tested and isn't broken in any obvious way, especially while making changes).

I'm trying to think of an equivalent for prose, and am coming up with examples like detecting conflicting descriptions of locations or named characters, or whether the author lost track of which character said which lines in the dialog.

> It's also not technically "unclear" in any notational sense

Perhaps not necessarily, but unfamiliar/borrowed/idiosyncratic notation is a perfect (and common) place for insufficient exposition to be hiding.

[0] https://imgur.com/gallery/ApzhVFj