4 ms·
That's what you can do with Coq. I can implement a reference interpreter and an optimized compiler and prove that the behavior of all possible programs are equi
by edejong 9y ago
That's what you can do with Coq. I can implement a reference interpreter and an optimized compiler and prove that the behavior of all possible programs are equivalent in both environments.
This is, what I assume, the long-term target of the article.
- DasIch 9y agoYou'd need to prove that a DBMS executes a query always correctly to begin with. That in itself would be quite the task. Additionally SQL as supported by some DBMSes (e.g. Postgres due to recursive CTE and window functions) is turing complete. That makes proving equivalency in general a bit challenging.