@nprofile1q... Another example of a 're-think' that would probably occur as a consequence of using a proof assistant is — the unscoped definition of syntax in IB Semantics and layering of typing derivations on top of raw syntax, etc., is going to be far too bureaucratic in any system. Not because of a limitation of the systems, but because of the fact that it *actually is* bureaucratic.

But if you start pulling this thread, you end up quickly doing things like revealing that type preservation is a stupid non-theorem (it should, and easily can, hold by definition) and that only *progress* is a real theorem of programming languages, which starts to undermine the overall ideology that has emerged around it...

Pulling these threads is good, but we also have to think about whether we may end up unpicking the entire sweater...