You are starting with an axiom that I'm talking nonsense and then bending everything I write in that direction instead of reading what I write. E.g.,

"I regret to say that that's not as easy as it sounds. There are issues of tractability, and more importantly, there's this not-quite-cottage industry of software development, which needs good-enough languages to use _today_."

I didn't say it was "easy", and clearly my point is progress and not current software development. Sure, for my project, I'm typing in code in Visual Basic .NET. For writing code today, all things considered for my context, that is about the best option.

But what I'm typing in is hardly different from what anyone might have typed in all the way back to Algol.

Here's the point: People type in all that code, and then what? Can some software go over it, report properties, do some transformations with known, useful properties? Not very much. Such things won't be better for Visual Basic than they were for Algol or anything between.

So, they type in the code, and then all they have is just that code. They can desk check it, test it, try it, revise it, etc., but it's all still digging the Panama Canal with a teaspoon one canal at a time. That is, there's no real automation and no significant exploitation of mathematical properties that could lead to automation.

Or, return to most of the rest of engineering where we have specifications of resistors, capacitors, inductors, transistors, fans, copper wire, steel sheets, aluminum bars, etc. with ohms, farads, density, tensile strength, electrical conductivity, etc. Okay, now compare with some DLL or its source code: What engineering properties do we have. Essentially none. It's like building with iron before we knew about tensile strength.

Sure, with some such research progress, eventually programmers would benefit. Obviously the intention is real progress in software productivity. We're not going to get such productivity by more of the same that got us C, C++, Java, Python, Visual Basic .NET, C#, etc.

Also for another of your points, I'm not talking about anything like branch prediction or deep pipelining. That's basically what to do with with the hardware to execute an existing instruction set.

Also the point is not math or not. The point is progress. Math will be necessary but not sufficient. That is, just stuffing in some math won't yield more than the old trick of putting two extra, unused transistors in a radio to claim nine transistors instead of seven.

Your point that there's a lot of good CS to do without 'mathematizing' the field is not promising for research or significant progress.