Re: does a safer language mean it is slower to run?

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 2023-10-25 20:01, robin vowels wrote:
> On Thursday, 8 June 2023 at 16:57:17 UTC+10, Niklas Holsti wrote:
>> On 2023-06-08 6:55, Nasser M. Abbasi wrote:
>>> Some folks in this thread
>>>
>>> https://discourse.julialang.org/t/comparison-of-rust-to-julia-for-scientific-computing/78508
>>>
>>> "I’m not an expert, but my feeling is that Rust is a “safer” language,
>>> which to me means it must be slower."
>>>
>>> etc..
>>>
>>> Some in that thread seem to argue that a safer language
>>> will/could be slower than otherwise.
>>>
>>> Since Ada is known to be one of the safest languages,
>>> do others here feel there is any truth to this?
>>>
>>> I thought that by having more type information in the language,
>>> the compile will be able to make more optimizations (because it
>>> know more), and hence the generated code should actually be
>>> faster, not slower with a language that is less safe?
>>>
>>> I am not a compiler expert but what do others here think?
> .
>> If a language needs run-time checks to ensure safety, those checks
>> usually take some time, making for slower execution.
> .
> Some language features need run-time checks.  These checks cannot be
> carried out at compile time.
> .
> PL/I has some features that require run-time checks.  When the computer
> hardware has certain facilities, that support does not take extra execution  time.
> For example, floating-point overflow and integer overflow are detected by the
> hardware on the IBM S/360 and subsequent machines including up to the latest
> System z.  Such detections cause an interrupt that can be handled by the PL/I
> program.  On the PC, integer overflow can cause an interrupt.
> .
>> If a language has a type system and compilation-time (legality) rules
>> such that the compiler can prove that some run-time checks are not
>> needed, that reduces or eliminates the slow-down. This is the case for Ada.
> .
> Range is not one of them.


/Some/ range checks in Ada can certainly be verified at compile time. 
For example:

    type ABCD is (A, B, C, D);
    subtype BCD is ABCD range B .. D;

    procedure Foo (X : in BCD)
    is
       Y : ABCD := X;
       Z : ABCD := ABCD'Pred(Y);
    ...

The initialization of Y formally involves a range check of X, but since 
BCD is a subtype of ABCD, the check can be elided at compile time. 
Likewise, the initialization of Z, with its computation of the Pred, 
formally includes a range check of Y, but since Y /= A can easily be 
proved, that range check can also be elided.

The most important type of check that can be elided at Ada compile time 
is array index check. Because arrays have specific index types in Ada, 
the compiler can often prove that the index expression will be in range.