Comment by Jtsummers
16 hours 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.
Right. I was actually quite surprised when i came across this paper/language and saw that it was from 2025.