> Most of those papers build insanely complex calculi to capture a simple idea that every junior engineer can understand in half a day.

Except that is working code. The insane complexity is almost never in the calculi themselves, but rather in the proofs that go along with them, to clearly show why the approach that has been taken to formalize that "simple idea" works as expected. That modeling work is quite essential if you want to ensure that the "simple" features in a programming language interact together in a sensible and useful way.