24 points | by azhenley 3 days ago ago
5 comments
For the curious, solvers like z3 are used in programming languages to verify logic and constraints. Basically it can help find logic issues and bugs during compile time itself, instead of waiting for it to show up in runtime.
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories...
The concept is called static analysis.
Seems adjacent, with some overlap.
in theory that's what a compiler is - a thin wrapper over a SAT solver. in practice most compilers just use heuristics <shrug>.
I was expecting a Z3 computer from Germany.
For the curious, solvers like z3 are used in programming languages to verify logic and constraints. Basically it can help find logic issues and bugs during compile time itself, instead of waiting for it to show up in runtime.
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories...
The concept is called static analysis.
Seems adjacent, with some overlap.
in theory that's what a compiler is - a thin wrapper over a SAT solver. in practice most compilers just use heuristics <shrug>.
I was expecting a Z3 computer from Germany.