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.
This is, what I assume, the long-term target of the article.
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.