I like the concept of separation logic as much as the next guy, but I don't think this is it. Just look at the examples, with loop invariants alone being longer than the whole example. It's not only a problem with ergonomics, but it leaves a lot of space for specification bugs.
And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.
And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.
Perhaps not, but C is still used in a lot of critical systems. Things like this for proving properties of some core of your program can be very helpful.
Comments
I like the concept of separation logic as much as the next guy, but I don't think this is it. Just look at the examples, with loop invariants alone being longer than the whole example. It's not only a problem with ergonomics, but it leaves a lot of space for specification bugs.
And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.
Perhaps not, but C is still used in a lot of critical systems. Things like this for proving properties of some core of your program can be very helpful.
Right. I was actually quite surprised when i came across this paper/language and saw that it was from 2025.