Where are we going from here? Software engineering needs formal methods

We’re starting to see this with commoditization/formalization of platforms. OS, storage, cloud, infrastructure, e-commerce are getting to the point where they’re pretty well explored. In another 20 years it’ll be so specialized and optimized that you’d need a Ph.D to make meaningful improvements in those areas.

So people won’t feel the need to try and recreate it themselves except for learning and as that process continues we’ll see those things formalize best practices which would eventually turn into engineering standards, etc…

You’ll have licensed and bonded engineers building low level highly formalized systems/services which meet certain guarantees. Similar to how I imagine civil engineering works.

Then for the rest of the industry you’ll have what we currently have which is like home construction where almost anything goes, but there are pieces that need to be validated by actual engineers or licensed professionals similar to how electricians and plumbers are licensed.

Our industry is not unique here. And many formal methods are hidden by the tools of the trade.

Physical engineering projects are not mathematically proven either. They are verified against some accepted set of tests using models that use various empirically measured properties for materials and the world around the project as proxies for how this will do, and include various factors like 1-in-N year events and some acceptable error margin or chance of failure.

In something like microprocessor design, the physical design and manufacturing of course can be wildly variable and difficult to characterize (as Intel has recently been finding out -- even on a very nicely running process line, variations can result in many devices not working at all, and those that do can have variations of tens of percent in major performance metrics (frequency, power consumption).

Go up a level to digital logic design. Like software there are formal methods for proving logic, but they are absolutely not used to "prove" the entire digital logic part of a CPU. That is much more like software than you might think, thousands of bugs get found and fixed. Many bugs (from performance to correctness) can even get found and after a chip has come back from the factory. They go through intensive verification cycles, and even then it's not at all uncommon for bugs to escape. Many "errata" are just noted and you live with them, some necessitate varying degrees of crippling performance or features (spectre, meltdown, transactional memory, etc). And some actually require new revisions of the product when the errors can't be corrected in firmware.

The only real difference between software and logic design is the cost of "recompiling" means they spend vast efforts with many angles and layers of ways to modify the behavior of a device after it is manufactured. This isn't something you can see, but there are thousands and thousands of dials and switches that can be set to change behaviour, from very low level (oops this bit of logic has a clock-gating bug, we need to flip the switch to disable clock gating for this particular group of gates it will cost 0.01mW of dynamic power), through logical behavior of various algorithms and structures in the chip, right up to higher level big hammers like microcode and micro traps (oops we didn't implement this instruction correctly, switch it to trap to microcode and we'll write a handler for it at a cost of 1% performance).

Is electrical engineering, microprocessor design, circuit design considered to be "not engineering"? Not by many.

Engineering is about applying structured methods to create something that solves problem. Software in some areas is ahead of the game here, using advanced version control tools and methodologies, continuous integration, although digital logic design has been starting to cotton on.

This is the real reason software is eating the world. Incumbents lose because aren't able to reorganize themselves around a software core, and so can't try things.

Formal methods are intrinsically satisfying, as are all quests for perfection and truth.