No. It's a car, and has the power to kill people on software malfunction, making it a critical system. Critical systems are tend to go through a much greater and more robust form of testing.
The destructive potential of a car exceeds that of a lot of handguns one can buy.
There have long been techniques for writing software as formal proofs of correctness. As far as I can tell, they haven't been popular with mainstream programmers because they are simply too different.
That is a really neat bit of fact; but, what does that have to do with what I was talking about? I really would like to know, it sounds like a really important insight, I'm just not sure what train of thought led to that.
