This tradeoff wasn't already an issue with languages like Modula and Ada.

As far as I am aware Ada is not memory safe without a runtime and with the presence of non-static memory. So you either have a runtime, no deallocation, or unsafety.

C also needs a runtime, it is called crt0 on UNIX and it is what calls main(), sets up global initialization functions (constructor functions in GCC C), emulates floating point,...

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.

OK, I should have said garbage collector, not runtime.

Are you claiming that Module-2 is memory safe?

What about:

  MODULE Boom

  VAR Foo : POINTER TO INTEGER;

  BEGIN
    Foo^ = 123;
  END Boom.

If I remember correctly that is a compiler error, because Foo is not initialized, so no 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.

Notice the use of IMPORT SYSTEM and SYSTEM.CAST, explicit, easy to search for, and to forbid via compiler switch (no unsafe code).

Yeah, I realized after posting that this would be a critique. I should have stipulated that it's a C syntactic language, which seems to be many peoples preference based on the most successful languages out there.

I never did much with Ada or Modula, so I won't claim to know anything more than their syntax, etc.

Rust still has no support for true formal analysis. It is therefore pointless to use it for high safety. Use a real theorem checker instead.

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.

Could this be used on the LLVM intermediate code?

http://www.cis.upenn.edu/~stevez/vellvm/

Good find. Likely yes.