Separation Logic
cacm.acm.org
cacm.acm.org
https://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.a...
This special topics course was held shortly before John Reynolds passed away.
(If you're bored, you can also see other things we have hosted on the same platform, including Deep Reinforcement Learning, Intro to ML, and the Computer Science Department holiday party :)
Specifically, there is a recent an analogue of SL, called incorrectness separation logic (ISL) that i designed to prove the presence of bugs, i.e. detect bugs:
https://link.springer.com/chapter/10.1007/978-3-030-53291-8_...
The main advantage of ISL is that it uses under-approximation, unlike original SL which uses over-approximation. That is to say, SL is used to show ALL program behaviours are correct, and in the process of doing so we may over-approximate the set of program behaviours. By contrast, ISL is used to show there are SOME incorrect (buggy) program behaviours.
ISL was implemented in a tool called PulseX at Facebook and shown to be a very scalable approach (comparable with and in some cases better than the state-of-the art Infer tool):
I probably meant it figuratively, huh? What I am saying after having keynoted at a Microsoft formal methods conference (as a critic) and after playing with TLS+ (which was educational) is that formal verification will make little impact on commercial systems because such systems are obliged to be built with inherently buggy components.
I am happy to acknowledge that progress is happening, yet the ultimate source of trouble is human ambition and impatience. How do you solve that?
Thankfully, this sort of analysis tends to use "constructive logic"; in which case, we're told why some property isn't provable (either because we're given a counterexample proving it's incorrect, or we're told which assumptions/preconditions need to be proved first)
"pretty much guaranteed to be incorrect"
... as it happens, SL (and infer) can be used to prove this too :) though that is more recent.
That's not what constructive logic means.
The reason constructive logic is nice for this is the first part: we'll be given a counterexample, or a total algorithm for generating counterexamples, etc. (depending on the nature of the statement and its quantifiers). This is preferable to classical logics, where an automated prover might tell us "false", but we have no idea why.
A logical description of what a piece of code does is evidently too much to ask of a working programmer. Instead, the prevailing dream is to just write code and then have some other code figure out what the first code actually does. Surely the sufficiently smart compiler is almost at hand.
This used to frustrate me and I suppose to some minor extent it still does. However, most of my frustration was relieved by Dijkstra's distinction between program correctness and program pleasantness. With vanishingly rare exceptions, revealed preferences show that industry could not care less about correctness. After all, it's pleasantness that determines success in the marketplace. Plenty of critically incorrect code nevertheless makes its owners billions. Sure, maybe all your private medical data and credit history got leaked, but here have a voucher for $10 a month worth of dark web monitoring for a year. I don't like this model, but at least it's in some sense rational.
Writing code is not about solving a problem perfectly but delivering solutions under economic constraints.
That's a good description of the Rust borrow checker, which is intended to be a sound analysis but a lot more restrictive than full separation logic.
If you can't use a tool without being an expert in it, the only people that will use that tool are experts and the techniques die out as the experts do.
It's a difficult problem that I believe has no globally optimal solution. However, I think there's fruitful research to be done in better recognizing what ought to be abstracted and what ought not to be in some domain specific sort of way. Informally we do this already. For example it's relatively common knowledge that one shouldn't leak username validity via timing attacks, so in that case the processing time cannot be abstracted away.
2. Apart from that, to me, if logic inspires (part of) the design of an analyzer, that's perhaps more valuable than using logic to judge it after the fact, as analysis design is hard; and this is true even if analyzer ends up following part of the spirit if not the letter of the logic.
I believe I get where you care coming from, though, and appreciate your perspective. :)