Hacker News Reader

Comment by diafygi | Hacker News Reader

There is. See the space shuttle software.

http://www.fastcompany.com/28121/they-write-right-stuff

It isn't a practical solution for the majority of software out there. I also think that while their method works, it is pretty archaic. Looking to the future I hope we can find a way to achieve the level of results they do, without the ridiculous effort and cost.

> Looking to the future I hope we can find a way to achieve the level of results they do, without the ridiculous effort and cost.

That is unlikely. For computational complexity theory reasons, writing correct software is extremely computationally expensive (regardless of whether or not the language is Turing complete). In fact, it is "the hardest problem in computer science", in the sense that any problem with bounded complexity can be efficiently reduced to software verification. Even verifying finite-state-machines (the simplest computational model) is PSPACE-hard.

What we can do is find many ad hoc ways, each helping to some extent with some kinds of correctness properties.

Most software problems I encounter in the real world ARE of bounded complexity, and they can be reduced to software verification. But this is still a very tedious process and there are significant gains to be had by making this more accessible without having to solve the hardest problem in computer science.

Certainly. It's just that there cannot be one (or a few) advances that would make writing correct programs generally easy. We can concentrate on domains (in the safety-critical embedded world this is almost a solved problem for some kinds of applications thanks to the invention of synchronous languages in the '80s, that make formal verification relatively efficient). We can also address some "internal" properties, like memory safety and transactions, that on the whole might make writing correct programs easier (though not provably correct).

I work on safety critical systems. At least 80% of the work for building such a system is not critical for the actual quality of the product, but is necessary to satisfy compliance rules. Documentation of the development process is really extensive.

And yet it still couldn't handle flying over new years: https://www.newscientist.com/article/dn10459-y2k-like-fears-...

It probably could and in testing it could, they just decided not to find out whether it would really work properly when seven people's lives depended on it working. If you can practically avoid an edge-case you haven't ever relied on in decades before when people's lives depend on it, not risking it doesn't seem that crazy.

Actually, they could but given the fact that the shuttle is not much different to strapping equipment and people to a gigantic bomb they seem to have decided that even though exhaustive testing found no issues a small change in the schedule was less risky.

Reply on news.ycombinator.com