|
|
|
|
|
|
by cwzwarich
4583 days ago
|
|
|
There are no automatically provable invariants that would cover SQLite's functionality. How does a tool automatically prove that a query compiler is correct, for example? I don't see an easy way, barring writing SQLite in Coq. |
|
|