Hacker News new | past | comments | ask | show | jobs | submit login

> 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-intege...




Let's say that through Why3 they manage to harness all kinds of SMT solvers (and others like grappa?).




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: