-------- Original Message --------

>> There is but C punts this to the OS mitigations like ASLR which in
>> Linux/Windows/BSDs case is even more of a performance hit than the targetted
>> runtime checks.
>
> ASLR by itself should have minimal to no performance impact on architectures
> with RIP-relative addressing. This excludes 32-bit x86 but x86-64 suffers no
> impact.
>

Maybe by itself at a basic level but some of ASLRs kernel patches seem quite
complicated with all the changes due to arms races like ROP defeating it and if
I recall correctly, Spectre affecting it etc.. Mitigations certainly have a
significant impact and are constantly getting more complex. Surely generalised
protections are either less effective and/or less performant than targetted ones.

>> Ada SPARK can have far more safety than Rust and have no performance hit at all.
>> I wonder how much faster it would be with the OS mitigations removed.
>
> What makes SPARK "far more" safe than Rust? As I understand both languages have
> some features that the other lack, but otherwise both are able to achieve full
> memory safety/defined behavior (and have an "escape hatch" for situations that
> warrant it).

Ada is quite comparable to Rust and in my opinion more secure due to it's
precision typing and more powerful concurrency features, whilst being easier to
use and read IMO. Ada SPARK lacks a borrow checker and some of the lifetime
complexities. Both rely to some degree on implementations for container security
for performance reasons. I won't talk about Ada SPARKS formal correctness
verification (Gold, Platinum) for safety (a much higher bar than security which
can replace unit tests) but Ada SPARK has an easier to use borrow checker than
Rust that also prevents memory leaks. It's bronze mode offers guaranteed safe
initialisation without requiring initialisation meaning a performance benefit.
It's silver mode can also be surprisingly easy to achieve offering proof the
code can not crash (absence of runtime error) and guarantee no
bounds/integer/buffer overflows will occur without any performance hit.

One of the best parts of SPARK is that you get all the niceties of Ada with high
level and low level and even high low level representation clauses but can
choose exactly what level of safety or performance any package has or even
sections of code (though packages make it easier to keep GNAT prove happy).

-- 
All the best,
             Kevin Chadwick