You're simply wrong to claim that we accept the situation without spending any real effort. In reality the more experienced developers who build abstraction layers tend to spend a lot of time trying to prevent leaks, but they can't have perfect foresight to predict what capabilities others will need. Software abstractions often last through multiple major generations of hardware technology with wildly different capabilities: you can't prevent those changes from leaking through to higher levels and it would be foolhardy to even try.

You cannot have a thing without doing the work to build it. You don't get the better abstraction without implementing it first. Your proof in theory, is just that, until exercised, and the divergence from the ideal to the real world is finally realized. I can teach a programmer all manner of linguistic trickery to allow them to exploit all sorts of mathematical abuse of notation. None of that makes a cotton-picking, salt-licking bit of difference if at the end of the day, if your symbolic proof isn't translateable to a machine code that runs and maps successfully onto the operational space of an implementation of a computing device. If you give a program written in the form of a Shakespearean sonnet (an example of a focus on radical novelty in encoding a program without regard to analogy); say; I still need a bloody compiler that'll turn that into something that is capable of running within the constraints of the machine, and the other primitives to make it work. That's TANSTAAFL. You break from what exists; you still have to reroot and establish a parallel basis of operation that covers the primitive operations you're familiar with. Djikstra might be right. There's something liberating to staying in the realm of the formal and mathematical. His detractor's were also right. He is so damn far above everyone else, that everybody in the room has trouble understanding just what it is he's going on about. At the end of the day, teach what the greatest number of the people there can firmly mentally grip, and pass that on. The geniuses like Djikstra will quickly outgrow it, and excel. They don't need the help. Everyone else on the other hand, does. I wouldn't be opposed, to trying Djikstra's approach myself. Shattering my current understanding of the practice of programming and working more from a formal methods POV. That comes after a career which has been fruitful, and was rooted in the old way which worked quite well for many others educated at the same time I was. I already know I can do it. His method just changes the emphasis. Though I will note with alarm, his reticence to test is disturbing. If he does assume everything is proofable from the get go, then I suppose you don't need tests; but that's hardly the way anything in the world actually bloody works. That's Math in a vacuum, with spherical cows. Not writing code then realizing "Shit, the processor in the machine I'm writing for doesn't support that primitive, or has a glitchy implementation thereof".

Software engineering isn't programming for people who can't; it's a set of practices and know-how to navigate a niche field that are battle hardened, and tested through time to actually guarantee some semblance of a chance of success in a field shaped by such fast development, the logic of 6 months ago seems antiquated. For that time with Moore's Law in full swing, yeah. Radical novelty might have been justifiable; but ultimately didn't push past the test of time. It can be as clever a hack as you can imagine, but if no one else can follow it... You haven't condensed it to a teachable form.