> 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 practicall

> 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 own https://blog.adacore.com/using-spark-to-prove-255-bit-integer-arithmetic-from-curve25519 https://blog.adacore.com/using-spark-to-prove-255-bit-intege...