Le 25/03/2026 à 19:09, David Hoppenbrouwers a écrit :
>
>> 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).

    Program correctness is not only about memory safety. Ada enforces
safety in many respects, such as methods to crash instead of producing a
wrong result. What I've read on SPARK is that it permits "formal
verification" of the program. Don't ask me what it exactly means: I've
retired 11 years ago and don't want to spend my time in things which
aren't a concern for me anymore. But it sounds like the ultimate quality
control.

    Note however that, between the program source and the executable,
there are several steps: language front-end, intermediate-code
optimisation, assembler generation, assembler optimisation, runtime
library, linker, link-time optimisation. These parts of the code
generation are written and reviewed by the smartest members of the
programmer's corporation, nevertheless, in some fields of activity,
people consider to review the machine code of the most critical parts.
Then there is always the issue of hardware bugs...

--     Didier