Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
potato-peeler
54 days ago
|
parent
|
context
|
favorite
| on:
Some silly Z3 scripts I wrote
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...
bjornsing
54 days ago
|
next
[–]
The concept is called static analysis.
ukuina
54 days ago
|
parent
|
next
[–]
Seems adjacent, with some overlap.
lkuty
53 days ago
|
prev
|
next
[–]
Like in the Dafny pogramming language. Cfr.
https://www.youtube.com/watch?v=oLS_y842fMc
mathisfun123
54 days ago
|
prev
[–]
in theory that's what a compiler is - a thin wrapper over a SAT solver. in practice most compilers just use heuristics <shrug>.
Consider applying for YC's Summer 2026 batch! Applications are open till May 4
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search:
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories...