[lmm]

> If a program halts, that is a narrow security issue that will not leak data.

Maybe. Depends what the fallback for the business that was using it is when that program doesn't run.

> Humans need to fix bugs, but that is nothing new. A memory bug with such features would be hardly more significant than any other bug

Perhaps. But it seems to me that the changes that you'd need to make to fix such a bug are much the same changes that you'd need to make to port the code to Rust or what have you, since ultimately in either case you have to prove that the memory access is correct. Indeed I'd argue that an approach that lets you find these bugs at compile time rather than run time has a distinct advantage.

[wakawaka28]

>Perhaps. But it seems to me that the changes that you'd need to make to fix such a bug are much the same changes that you'd need to make to port the code to Rust or what have you, since ultimately in either case you have to prove that the memory access is correct.

No, you wouldn't need to prove that the memory access is correct if you relied on hardware features. Or I should say, that proof will be mostly done by compiler and library writers who implement the low level stuff like array allocations. The net lines of code changed would definitely be less than a complete rewrite, and would not require rediscovery of specifications that normally has to happen in the course of a rewrite.

>Indeed I'd argue that an approach that lets you find these bugs at compile time rather than run time has a distinct advantage.

It is an advantage but it's not free. Every compilation takes longer in a more restrictive language. The benefits would rapidly diminish with the number of instances of the program that run tests, which is incidentally one metric that correlates positively with how significant bugs actually are. You could think of it as free unit tests, almost. The extra hardware does have a cost but that cost is WAAAY lower than the cost of a wholesale rewrite.

[lmm]

> No, you wouldn't need to prove that the memory access is correct if you relied on hardware features. Or I should say, that proof will be mostly done by compiler and library writers who implement the low level stuff like array allocations. The net lines of code changed would definitely be less than a complete rewrite, and would not require rediscovery of specifications that normally has to happen in the course of a rewrite.

I don't see how the hardware features make this part any easier than a Rust-style borrow checker or avoid requiring the same rediscovery of specifications. Checking at runtime has some advantages (it means that if there are codepaths that are never actually run, you can skip getting those correct - although it's sometimes hard to tell the difference between a codepath that's never run and a codepath that's rarely run), but for every memory access that does happen, your compiler/runtime/hardware is answering the same question either way - "why is this memory access legitimate?" - and that's going to require the same amount of logic (and potentially involve arbitrarily complex aspects of the rest of the code) to answer in either setting.