"Bob Noel" wrote in message
...
What we don't have is the ability to formally prove the correctness of
software.

We DO have the ability to prove "correct enough". That is, we have
engineering strategies designed to ensure correctness to some given degree.
These are the same techniques that were used for the space shuttle computers
(though, unfortunately, not for recent unmanned space probes), and similar
techniques are used for existing automation in aviation.

It's true that we don't have mathematical proofs for correctness. Of
course, it's widely believed we may never be able to have that. But
physical engineering suffers from similar limitations, and it seems to get
by just fine. Theoretical design can always be undermined by human
implementation, but there is an idea of "good enough" in both types of
engineering. You simply design in assumptions of human failure of
implementation.

I don't see this as a fundamental barrier to pilotless airliners.

Pete