alt Hacker NewsCute. 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.
Replies
> 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.
> 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.
Oddly they didn't even reuse the annotation for this that GCC already has: https://stackoverflow.com/questions/18485447/gcc-attribute-m...