3 ms·
Most of all, because if you can prove that two queries are equivalent in behavior, you are close to proving that one DBMS has the same behavior as another DBMS
by edejong 9y ago
Most of all, because if you can prove that two queries are equivalent in behavior, you are close to proving that one DBMS has the same behavior as another DBMS for all possible SQL queries.
And then you ask: Why?
Well, if you can prove two DBMSs equal for all SQL queries, you can prove that an optimization to the DBMS (such as an improvement to the query optimizer or new indexing systems) will not affect the behavior of any possible SQL you provide.
- DasIch 9y agoThat's not at all what this does and it's not possible to do either.
- heng222 9y agoIt'll be possible if both databases are written using proof assistants like Coq. And I think this work is a step towards that direction.
- edejong 9y agoThat'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.