[mirker]

I agree you can make software rigorous like in ME. The part which is hard is that debugging or proving properties about a program is much more difficult than writing the program. These costs are currently hard to amortize over multiple projects. Real-time systems have some of these facets (e.g., spacecraft).

For example, a memory allocator can be studied in the usual algorithmic sense or perhaps how they impact the stability of the system under randomized load. Can you prove the system remains stable? Yeah. Is it worth it when you can reboot machines and add some heuristics? No.

Currently, the big places which are getting any attention for verification of functionality are embedded applications and OS kernels. Even then, the depth of verification is limited to common bug categories.