23 ms·

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

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?).

leecommamichael 2y ago
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?
- pjc50 2y ago
  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).
  - milesrout 2y ago
    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 2y ago
      > 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 2y ago
        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 2y ago
        Reread my comment. You are confusing proof and fact.
  - chillingeffect 2y ago
    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 2y ago
      The problem is that people are really bad at that kind of precision.
  - AnimalMuppet 2y ago
    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 2y ago
      I suspect seL4 could be proven correct only because it uses simple lifetime patterns.
- crabbone 2y ago
  > 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).
nottorp 2y ago
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.
- GoblinSlayer 2y ago
  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 2y ago
    Pascal being derived from Algol, it makes a lot of sense.
- znpy 2y ago
  > 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 https://www.embarcadero.com/products/delphi/features/design
  - AnimalMuppet 2y ago
    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 2y ago
      my bad, i might have missed the sarcasm then :)
- pjmlp 2y ago
  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".

leecommamichael 2y ago

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?

pjc50 2y ago
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).
- milesrout 2y ago
  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 2y ago
    > 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 2y ago
      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 2y ago
      Reread my comment. You are confusing proof and fact.
- chillingeffect 2y ago
  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 2y ago
    The problem is that people are really bad at that kind of precision.
- AnimalMuppet 2y ago
  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 2y ago
    I suspect seL4 could be proven correct only because it uses simple lifetime patterns.
crabbone 2y ago
> 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).

nottorp 2y ago

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.

GoblinSlayer 2y ago
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 2y ago
  Pascal being derived from Algol, it makes a lot of sense.
znpy 2y ago
> 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 https://www.embarcadero.com/products/delphi/features/design
- AnimalMuppet 2y ago
  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 2y ago
    my bad, i might have missed the sarcasm then :)
pjmlp 2y ago
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".