Hacker News Reader

You're right that formal methods do not guarantee absence of 'errors' in the sense of unforseen unwanted behavior.

But formal methods, which typically are based on computer-checked proofs, can help you to eliminate certain possibilities. They are severely underestimated and underused because of our dependence on C.

The formal methods do not 'fail' as such. They just fail to prove anything boyond the proven property. Such properties can very well (and often do) include failure (of whatever kind) of parts in the system.

Apart from AI, which as an approach to embedded systems is almost by definition the opposite, I only see one way forward from the mess we're in now: formal methods.

That's why aerospace electronics have temporal and physical redundancy as well as voting algos. These generally rule out the radiation, physical damage, and RF issues.

The issue wasn't that the error happened. The issue was Toyota did not do proper due diligence to prevent errors.