Hacker News new | ask | show | jobs
by trenchgun 1335 days ago
It is on fact possible to write provably correct software for safety critical applications.

Not by testing, but by using formal methods.

2 comments

That's nice for the software. Now how about the hardware? How about the electronic hardware's not-exposed firmware, does that count? Did the subcontractor test it for three years at 10,000 feet for radiation-induced bit-flips? With or without lightning strikes?
> How about the electronic hardware's not-exposed firmware, does that count? Did the subcontractor test it for three years at 10,000 feet for radiation-induced bit-flips? With or without lightning strikes?

Blast the module in a radiation chamber. It can be done, it's only extremely expensive - the military has the budget (makes sense, given that a fighter jet or a bomber should be able to power through a nuclear bomb fallout), but civilian airliners are all about cost efficiency.

Including a system reboot, on the ground, as part of your on going maintenance activities is a fault, or incorrect software.
Is a roof you have to redo every 20 years, or a paint that only lasts 10 years faulty? Is a car that needs brakes replaced every X thousand kilometers faulty?

It is only faulty if it does not run according to spec, or if you it run outside the spec.

Exactly. If the manual says "reboot every 51 hours", you do just that and all is fine. If you have to reboot every, say, 25 hours, something is broken.