3 ms·
There are no automatically provable invariants that would cover SQLite's functionality. How does a tool automatically prove that a query compiler is correct, fo
by cwzwarich 13y 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.