With Rust this tradeoff of safe-with-runtime vs. unsafe-without-runtime is no longer your only choice. Now you can choose safe-with-strong-compiler-no-runtime...
As for Ada, you can selectively disable which parts of the runtime actually land on the generated executable via compiler pragmas.
Deallocation can be done via pools or controlled types.
What about:
MODULE Boom
VAR Foo : POINTER TO INTEGER;
BEGIN
Foo^ = 123;
END Boom.But if you still want to get your point through and have a boom.
MODULE Boom;
IMPORT SYSTEM;
VAR Foo : POINTER TO INTEGER;
BEGIN
Foo := SYSTEM.CAST(POINTER TO INTEGER, 43414);
Foo^ := 123;
END Boom.
I never did much with Ada or Modula, so I won't claim to know anything more than their syntax, etc.
Now Rust as a target for compiling proofs into a programming language is pretty nice. Safe code can have no aliasing due to borrow checker (which should also be formally verified). Threading issues are vastly simplified, though fairness still has to be verified, as well as a few other properties.