This is short but sweet. I absolutely love to see when approaches like this catch real bugs! It’s one thing to talk about correctness in theory, but people’s eyes tend to glaze over when it’s not connected to their daily life.
I don’t think it’s controversial to say that any non-verified piece of code has at least a handful of legitimate bugs (not counting “bugs” from misspecification which are unavoidable). Sure, a subset of those might be so rare or trivial that it might not matter too much during everyday usage, but don’t we observe in practice that any given enough time and users all bugs eventually get hit?
That probability has to be amplified for systems software as well, e.g. compilers and OS’s, since every piece of software has to touch these at some point. Long story short, thank the lord that our formal verification tools and techniques have taken a major leap forward in recent years, because there’s a lot of software that we actually need it for.
This is short but sweet. I absolutely love to see when approaches like this catch real bugs! It’s one thing to talk about correctness in theory, but people’s eyes tend to glaze over when it’s not connected to their daily life.
I don’t think it’s controversial to say that any non-verified piece of code has at least a handful of legitimate bugs (not counting “bugs” from misspecification which are unavoidable). Sure, a subset of those might be so rare or trivial that it might not matter too much during everyday usage, but don’t we observe in practice that any given enough time and users all bugs eventually get hit?
That probability has to be amplified for systems software as well, e.g. compilers and OS’s, since every piece of software has to touch these at some point. Long story short, thank the lord that our formal verification tools and techniques have taken a major leap forward in recent years, because there’s a lot of software that we actually need it for.