> It does not matter at which point the unsafe action is stopped.

It does in practice. With a compile time check the issue simply cannot happen, and there is no need to deal with it in the code or at system level.

With a runtime check the issue may happen, but will be detected when it does. Still, the choice then is either to crash or to deal with it with some runtime recovery action. Either way has some cost: the system around the executable must deal with more crashes, or the code gets more complex (and sometimes more brittle, even if the intention is the opposite).

Only the compile time check makes an issue really go away. This is to me the attraction of strong typing and any form of compilation time check. There's a price to pay too in accepting the related constraints: type checking must pass. So there's a cost here too. For complex or sensitive applications I personally much prefer this upfront cost.

But it's definitely not the only way: Erlang has runtime type checks, but a very good runtime error handling framework (the reference?), and it works well. Still, most environment relying on runtime checks are not at this level.

>Only the compile time check makes an issue really go away.

The issue that goes away in both cases is the issue of unsafe memory access. There are disadvantages to runtime checks, as you mention, but there is no difference in the level of safety achieved.

You need to consider not just the memory access itself, but the consequences of preventing it.

With a compile time check, there's a development cost but absolutely no runtime consequence.

With a dynamic check, sure the memory access is detected and blocked. But if you stop there the application crashes, which may be completely unacceptable. In an embedded system such a crash may be as bad as the incorrect access itself.

More generally, the issue is not so much the incorrect access than its possible adverse consequences. With a compile time check, there are no runtime consequences. With a runtime check, there are still runtime consequences: either the impact of an application crash, or the extra error handling code and behavior to deal with the detected wrong access and mitigate it at runtime. Whether such consequences are acceptable or not depends on the context, but it's there and do make a difference with a compile time or static analysis check.

>In an embedded system such a crash may be as bad as the incorrect access itself.

I don't agree on this point. An incorrect access on an embedded system has the potential to cause all kinds of horribly subtle bugs involving memory corruption. A simple crash is generally much better.

Possibly, but I won't argue about hypothetical kinds of bad when a runtime issue happen ;) The point I tried to make was that you want neither for such use cases. Hence compile time verification (type base, static analysis, proofs for the most critical).