3 ms·

Cute. They've introduced ownership to C. The annotation system is expressing ownership, in a rather clunky way. You have to explicitly declare that functions cr

by Animats 10mo ago

Cute. They've introduced ownership to C. The annotation system is expressing ownership, in a rather clunky way. You have to explicitly declare that functions create or release allocated space. That's ownership tracking. But "We currently model all buffers as infinitely-sized. We will be adding out-of-bounds checking soon." That's the hard problem.

LiamPowell 10mo ago
> But "We currently model all buffers as infinitely-sized. We will be adding out-of-bounds checking soon." That's the hard problem. It's not particularly difficult for the prover. You essentially just need to do a translation from C in to your ATP language of choice, with a bunch of constraints that check undefined behaviour never occurs. Tools such as Frama-C and CBMC have supported this for a long time. The difficult part is for the user as they need to add assertions all over the place to essentially keep the prover on the right track and to break down the program in to manageable sections. You also want a bunch of tooling to make things easier for the user, which is a problem that can be as difficult as you want it to be since there's always going to be one more pattern you can detect and add a custom handler/error message for.
- Animats 10mo ago
  > It's not particularly difficult for the prover. I know that. Did that decades ago. I wanted to see how they did the annotations and proofs. What can you express? Partially filled arrays are moderately hard. Sparsely initialized arrays need a lot of scaffolding. This is an area where most "safe C" variants have foundered.
rwmj 10mo ago
Oddly they didn't even reuse the annotation for this that GCC already has: https://stackoverflow.com/questions/18485447/gcc-attribute-malloc https://stackoverflow.com/questions/18485447/gcc-attribute-m...
1718627440 10mo ago
> Cute. They've introduced ownership to C. Ownership semantics are described in every serious C interface. Linters for checking it have also existed for decades. I find the notion that Rust invented it to be incredible stupid. Rust just has different ownership semantics and makes it an enforced part of the language (arguable a good idea). And yes they of course also do bounds-checking.
- pjmlp 10mo ago
  Rust did not invent affine types of course, those that affirm that lack background in type systems.

by Animats 10mo ago

LiamPowell 10mo ago

> But "We currently model all buffers as infinitely-sized. We will be adding out-of-bounds checking soon." That's the hard problem. It's not particularly difficult for the prover. You essentially just need to do a translation from C in to your ATP language of choice, with a bunch of constraints that check undefined behaviour never occurs. Tools such as Frama-C and CBMC have supported this for a long time. The difficult part is for the user as they need to add assertions all over the place to essentially keep the prover on the right track and to break down the program in to manageable sections. You also want a bunch of tooling to make things easier for the user, which is a problem that can be as difficult as you want it to be since there's always going to be one more pattern you can detect and add a custom handler/error message for.

Animats 10mo ago
> It's not particularly difficult for the prover. I know that. Did that decades ago. I wanted to see how they did the annotations and proofs. What can you express? Partially filled arrays are moderately hard. Sparsely initialized arrays need a lot of scaffolding. This is an area where most "safe C" variants have foundered.

rwmj 10mo ago

Oddly they didn't even reuse the annotation for this that GCC already has: https://stackoverflow.com/questions/18485447/gcc-attribute-malloc https://stackoverflow.com/questions/18485447/gcc-attribute-m...

1718627440 10mo ago

> Cute. They've introduced ownership to C. Ownership semantics are described in every serious C interface. Linters for checking it have also existed for decades. I find the notion that Rust invented it to be incredible stupid. Rust just has different ownership semantics and makes it an enforced part of the language (arguable a good idea). And yes they of course also do bounds-checking.

pjmlp 10mo ago
Rust did not invent affine types of course, those that affirm that lack background in type systems.