My takeaway with formal verification tools is that they are leaky abstractions. Sure, I can write a contract to prove a function's implementation but the moment Z3 takes too long to run, I need to peek into the tool is implemented and if there are any bugs in my triggers for quantifier instantiations.
I agree with parent. In an ideal world, I should not have to take graduate level coursework to prove a function's correctness. Sometimes, the programs I'm trying to verify are not proof-friendly, so I end up redoing my data structures just to make the proofs go through.
Comments
My takeaway with formal verification tools is that they are leaky abstractions. Sure, I can write a contract to prove a function's implementation but the moment Z3 takes too long to run, I need to peek into the tool is implemented and if there are any bugs in my triggers for quantifier instantiations.
I agree with parent. In an ideal world, I should not have to take graduate level coursework to prove a function's correctness. Sometimes, the programs I'm trying to verify are not proof-friendly, so I end up redoing my data structures just to make the proofs go through.