7 ms·

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 comp

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#Verification https://en.wikipedia.org/wiki/Satisfiability_modulo_theories...

bjornsing 7mo ago
The concept is called static analysis.
- ukuina 7mo ago
  Seems adjacent, with some overlap.
mathisfun123 7mo ago
in theory that's what a compiler is - a thin wrapper over a SAT solver. in practice most compilers just use heuristics <shrug>.
lkuty 7mo ago
Like in the Dafny pogramming language. Cfr. https://www.youtube.com/watch?v=oLS_y842fMc https://www.youtube.com/watch?v=oLS_y842fMc