[flitzofolov]

Makes sense, good luck! I know that sounds snarky, I'm looking forward to rational progress and cooperation on the evolution and adoption of the standard. Just haven't seen that played out in such a planned orderly fashion yet (ipv6?).

[nottorp]

ipv6, unicode, usb...

Why am I more worried than excited about a new standard?

By the way bounds checking was introduced in Turbo Pascal in 1987. Iirc people ended up disabling it in release builds but it was always on in debug.

But ... it's Pascal, right? Toy language.

[pjmlp]

Bounds checking exists at very least since JOVIAL in 1958, or if you consider FORTRAN compilers have add an option for bounds checking for quite some time, 1957.

Here is my favourite quote, every time we discuss bounds checking.

"A consequence of this principle is that every occurrence of every subscript of every subscripted variable was on every occasion checked at run time against both the upper and the lower declared bounds of the array. Many years later we asked our customers whether they wished us to provide an option to switch off these checks in the interests of efficiency on production runs. Unanimously, they urged us not to--they already knew how frequently subscript errors occur on production runs where failure to detect them could be disastrous. I note with fear and horror that even in 1980 language designers and users have not learned this lesson. In any respectable branch of engineering, failure to observe such elementary precautions would have long been against the law."

-- C.A.R Hoare's "The 1980 ACM Turing Award Lecture"

Guess what programming language he is referring to by "1980 language designers and users have not learned this lesson".

[znpy]

> But ... it's Pascal, right? Toy language.

Not really.

It's just out of fashion. But there are really high quality current day implementation, like the one from Embarcadero (i think they acquired Borland a while ago?): https://www.embarcadero.com/products/delphi/features/design

[AnimalMuppet]

I think nottorp was being a bit sarcastic. I think the point was, if Pascal, which some in the C/C++ world regard as a "toy" language, had this in 1987, maybe we can actually think about having it in "real" languages in 2025.

[znpy]

my bad, i might have missed the sarcasm then :)

[GoblinSlayer]

I heard algol had bounds checking somewhere in 60s as an implementation feature. Reportedly customers liked it a lot that the programs don't produce wrong results faster.

[nottorp]

Pascal being derived from Algol, it makes a lot of sense.

[leecommamichael]

Yeah, I’m wondering what this even means. I’m assuming they’ll have to define “memory safety” which is already quite the task. Memory safe in what context? On what sort of machine? What sort of OS?

[crabbone]

> On what sort of machine? What sort of OS?

Just sharing an anecdote: recently, I had to create Linux images for x86 on ARM machine using QEMU. During this process, I discovered that, for example, creation of initrd fails because of memory page size (some code makes assumption about page size and calculates the memory location to access instead of using system interface to discover that location). There's a similar problem when using "locate" utility. Probably a bunch more programs that have been successfully used millions, well, probably trillions times. This manifests itself in QEMU segfaulting when trying to perform these operations.

But, to answer the question: I think, one way to define memory safety is to ensure that the language doesn't have the ability to do I/O to a memory address not obtained through system interface. Not sure if this is too much to ask. Feels like for application development purposes this should be OK, and for system development this obviously will not work (someone has to create the system interface that supplies valid memory addresses).

[pjc50]

I think the usual context just requires language soundness; it doesn't depend on having an MMU or anything like that. In particular, protection against:

- out-of-bounds on array read/write

- stack corruption such as overwriting the return address

It doesn't directly say "you can't use C", but achieving this level of soundness in C is quite hard (see sel4 and its Coq proof).

[chillingeffect]

Everyone picks on C, but we have a standard for this. We've been following it for decades in regulated industries. If people take the time, it can be perfectly safe. It requires thinking of a computer as a precision machine, rather than a semantic "do what i'm thinking" box.

[timw4mail]

The problem is that people are really bad at that kind of precision.

[AnimalMuppet]

Maybe I lack vision in such matters, but: how would you corrupt the stack without an out-of-bounds write?

But there's another aspect that I think you missed: use after free.

As you say, achieving this level of soundness with C is hard. Proving it is much harder. (Except, how do you know you've achieved it if you don't prove it?)

[GoblinSlayer]

I suspect seL4 could be proven correct only because it uses simple lifetime patterns.

[milesrout]

Yet that is not what memory safety means. A program being memory safe or not depends on its actual behaviour not what you can prove about that behaviour. There are plenty of safe C programs and plenty of unsafe ones. Proving something is safe doesnt make it safe.

Also these properties are a very small subset of general correctness. Who cares if you write a "safe" program if it computes the wrong answer?

[pjc50]

> Proving something is safe doesnt make it safe.

Err .. that is actually the point of the proof. Can you give an example of something with a Coq-type safety proof that has a memory safety bug in it?

[baq]

Not OP but you can in theory add cosmic rays, rowhammer attacks and brownout/undervolt glitching into the mix. Kinda stretching it but sometimes you have to think about these.

[milesrout]

Reread my comment. You are confusing proof and fact.