Everyone who writes safety critical software should read this

[Andrei Alexandrescu]

On 11/2/13 9:49 AM, bearophile wrote:
> Andrei Alexandrescu:
>
>> I'm unclear on why you seem so eager to grind that axe.
>
> Because I've tried the alternative, I've seen it catch bugs (unwanted
> integral overflows) in my code that I was supposing to be "good", so I
> will never trust again languages that ignores the overflows. And if we
> talk about high integrity software, D integrals management is not good
> enough.

I disagree.

>> The matter seems to be rather trivial - disallow statically the use of
>> built-in integrals, and prescribe the use of library types that do the
>> verification. A small part of the codebase that's manually verified
>> (such as the library itself) could use the primitive types. Best of
>> all worlds. In even a medium project, the cost of the verifier and
>> maintaining that library is negligible.
>
> How many C++ programs do this? Probably very few (despite now Clang is
> able to catch something in C code). How many Ada programs perform those
> run-time tests? Most of them.

That has to do with the defaults chosen. I don't think "mission 
critical" is an appropriate default for D. I do think that D offers 
better speed than Ada by default, and better abstraction capabilities 
than both C++ and Ada, which afford it good library checked integrals. I 
don't see a necessity to move out of that optimum.

>> A small part of the codebase that's manually verified (such as the
>> library itself) could use the primitive types.
>
> In some cases you want to use the run-time tests even in verified code,
> to guard against hardware errors caused by radiations, noise, etc.

How is this a response to what I wrote?

>> We need to get SafeD up to snuff!
>
> At the moment safeD means "memory safe D", it's not "safe" regarding
> other kinds of problems.
>
> "Undefined operations" are lines of code like this, some of them are
> supposed to become defined in future D:
>
> a[i++] = i++;
> foo(bar(), baz());
> auto x = int.max + 1;
>
> and so on.

Agreed, this is not part of the charter of SafeD. We need to ensure 
left-to-right evaluation semantics through and through.

>> But I should hope D would have a safety edge over C.
>
> Of course :-) Idiomatic D code is much simpler to write correctly
> compared to C code (but in D code you sometimes write more complex code,
> so you have a little of bug-proneness equalization. This is a part of
> the human nature).
>
> There are many levels of safety, high integrity software is at the top
> of those levels (and probably even high integrity software has various
> levels: some submersibles guide software could be not as bug free as
> software of the Space Shuttle guiding system) is a very small percentage
> of all the code written today.

And to take that to its logical conclusion, we don't want the defaults 
in the D language to cater to such applications.


Andrei