> turn some problems from intractable to tractable, or from "go and get a coffee" to "interactive HTTP call"
Or broaden the set of problems that can practically be attacked using SAT solvers.
Deductively proving program-correctness is one such problem. It's currently possible but clunky, [0] or put another way, it's practical given a patient and skilled user. Further advances in solvers will presumably translate into 'lowering the bar' for automated correctness proving.
[0] With the disclaimer that I'm not an expert, this quote seems to capture the state of things in Ada SPARK: none of the provers available in SPARK (CVC4, Z3 and Alt-Ergo) are able to prove the entire project on their ownhttps://blog.adacore.com/using-spark-to-prove-255-bit-intege...
Or broaden the set of problems that can practically be attacked using SAT solvers.
Deductively proving program-correctness is one such problem. It's currently possible but clunky, [0] or put another way, it's practical given a patient and skilled user. Further advances in solvers will presumably translate into 'lowering the bar' for automated correctness proving.
[0] With the disclaimer that I'm not an expert, this quote seems to capture the state of things in Ada SPARK: none of the provers available in SPARK (CVC4, Z3 and Alt-Ergo) are able to prove the entire project on their own https://blog.adacore.com/using-spark-to-prove-255-bit-intege...