In order for this argument to hold, we would have to live in a world where no one has created a safe language with no runtime.

We don't live in such a world, fortunately.

I don't think we are talking about the same thing at all.

Many people say "no runtime" to mean "small runtime like C or C++ have" rather than literally no runtime. This is due to the confusion around interpreters sometimes being called "runtimes."

The Rust runtime is larger than C's (I imagine it's not much larger than C++, but this is already way too large). AFAIK, nobody ever proved it works as designed. The fact that it's design is not very stable is also a problem.

Now, with some more thought about it, C itself is not a great target for correctness proofs. Too much is left unspecified, and there is little agreement over some of the lower level stuff. A simplified version of Rust might be a better target than C, if somebody ever creates it, but a lot of the safety would have to be left out of it.

Rust also lets you write a custom runtime by specifying a start function if you want.

> The fact that it's design is not very stable is also a problem.

Rust is stable.

I believe that it is smaller than C++'s but larger than C's, but I'm not a mega expert here. I used to know where those files were located in-tree, but don't anymore.

I think there's also several distinctions you can draw here; for example, strictly speaking, almost no runtime is required, but if you're using say, the standard library, you still might end up with a bunch of code. The actual requirements are very small though.

> AFAIK, nobody ever proved it works as designed. The fact that it's design is not very stable is also a problem.

Sorry, I don't understand what you mean here. The runtime?

> A simplified version of Rust might be a better target than C, if somebody ever creates it, but a lot of the safety would have to be left out of it.

I _think_ with the above comments, you mean the Rust langauge overall, not the runtime, right? So, Rust _is_ very stable; post 1.0 we have made extremely small breaking changes, corresponding to the way new C++ standards sometimes introduce minor technical backwards incompatibilities. As for correctness proofs, there are multiple academic institutions working on it; and they don't have to "leave the safety out"; that's what they're trying to prove!

Finally, we link to jemalloc, which is an additional bit of runtime of its own (which can be turned off with alloc_system)

There's also compiler-rt which does some of the eh stuff for panics and whatnot.

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.

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