3 ms·
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
by IsTom 23d ago
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.
- Jtsummers 23d ago> 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.
- rramadass 23d agoRight. I was actually quite surprised when i came across this paper/language and saw that it was from 2025.