Mission-Critical systems

[mw]

On Friday, 19 March 2021 at 06:32:18 UTC, Walter Bright wrote:
> On 3/16/2021 8:44 PM, tsbockman wrote:
>> So, definitely use LDC if you are planning to bet human lives 
>> and/or millions of dollars on it working fully correctly.
>
> The first three years of my career was spent developing the 
> flight critical stabilizer trim gearbox for the 757. Flight 
> critical means if it comes apart, you lose the airplane and 
> everyone aboard.
>
> So I know how to build things that are critical for human life.
>
> Generally speaking, there is no relying on any tool to be 
> bug-free. Test and verify everything. Design in a backup system 
> to monitor the behavior.

...

> Notice there is no reliance on bug-free hardware, bug-free 
> algorithms, bug-free code, bug-free compilers, etc.

In engineering practice, redundancy backup is the way to achieve 
reliability.

On the other hand, programming logic / compiler is also 
mathematics, where reliability is achieved by theorem provers, 
e.g.


https://en.wikipedia.org/wiki/CompCert

https://github.com/AbsInt/CompCert

CompCert

The formally-verified C compiler.

The distinguishing feature of CompCert is that it has been 
formally verified using the Coq proof assistant: the generated 
assembly code is formally guaranteed to behave as prescribed by 
the semantics of the source C code.