Program logic bugs vs input/environmental errors

[via Digitalmars-d]

On Saturday, 4 October 2014 at 08:25:22 UTC, Walter Bright wrote:
> On 10/3/2014 9:10 AM, "Ola Fosheim Grøstad" 
> <ola.fosheim.grostad+dlang at gmail.com>" wrote:
>> I think Walter forgets that you ensure integrity of a complex 
>> system of servers
>> by utilizing a rock solid proven transaction 
>> database/task-scheduler for
>> handling all critical information. If that fails, you probably 
>> should shut down
>> everything, roll back to the last backup and reboot.
>
> You don't ensure integrity of anything by running software 
> after it has entered an unknown and unanticipated state.

Integrity is ensured by the transaction engine. The world outside 
of the transaction engine has NO WAY of affecting integrity.

D code that is written today belongs outside the transaction 
engine.

> There's no way you'd bet your life on it.

SAAB Gripen crashed in 1989 and 1993 due to control software, the 
pilots used their parachutes and sent the plane in a safe 
direction. Eurofighter is wire controlled, you most likely cannot 
keep it stable without electronic control. So if it fails, you 
have to use the parachute. Bye, bye $100.000.000.

Anyway, failure should not be due to "asserts", that should be 
covered by program verification and formal proofs. Failure can 
still happen if the stabilizing model is inadequate.

During peace time fighter jets stay grounded for many days every 
year due to technical issues, maybe as much as 50%. In war time 
they would be up fighting… So yes, you bet your life on it when 
you defend the air base. Your life is worth nothing in certain 
circumstances. It is contextual.

> I think you forget my background in designing critical flight 
> controls systems. I know what works, and the proof is the 
> incredible safety of airliners. Yeah, I know that's "appeal to 
> authority", but I've backed it up, too.

That's a marginal use scenario and software for critical control 
systems should not rely on asserts in 2014. Critical software 
should be formally proven correct.