Hacker News Reader

Comment by pcwalton | Hacker News Reader

> In the coming decades as the automation and ease-of-use of formal verification tools improves, I think C may well end up being the best choice for security-critical and correctness-critical systems programming. With current tools it is already ahead of Ada, C++, and Rust.

The problem is that in practice when people reach for C, they reach for stb_image.h, not formal verification packages that are expensive and used for approximately no software in mainstream use outside of fields like avionics. The economics of formal verification just don't work for mainstream software. Organizations are simply not willing to multiply their development costs by 10x or 100x.

View on HN

> Organizations are simply not willing to multiply their development costs by 10x or 100x.

I think this is a valid point today. Will it remain so in the future?

If say liabilities for bugs in critical software shift or if natsec regulations require software that touch infra like: water, power, telecom, and mass transit to be verified like avionics software is. IMO both are likely 2-3 decades out.

Either or both of these happening will expand demand for more hardened platform-level code.

>If say liabilities for bugs in critical software shift or if natsec regulations require software that touch infra like: water, power, telecom, and mass transit to be verified like avionics software is. IMO both are likely 2-3 decades out.

This can be mitigated by designing robust systems that are robust to flaws of its components. There is an understanding that bugs or corruption way happen and the system should able to tollerate it and fix itself or alert people that something is wrong or needs to be addressed.

It doesn't seem plausible to me that an organization that refuses to create reliable components will create reliable systems out of the components.

It's cheaper to be able to handle your program crashing every once and a while than to try and earliest 100% of all crashes from your program. It's possible to deal with situation where you know you are never going to be 100% bug free.

I have yet to see something like that remaining robust to unauthorized memory access.

The thing is software is made to compete for new monopolies rather than to perform functions reliably. There's so much funding for monopoly-rent-seeking that this dominates and characterizes the field. Correctness just isn't that important for that.

Over time, perhaps the available monopolies will dry up, a few megafirms will buy up everything that can collect rents, and the only software left to write will be practical.

Reply on news.ycombinator.com