Every verification needs a spec, and in this case the spec is the Postgres implementation. I think we can and should do a lot better than taking 2.6 million lines of C code as the spec.

In general, the spec must be human readable, and I believe to achieve that we must do away with SQL. Putting aside the thousands of pages of SQL standard, even the core subset has a gnarly semantics due to issues like nulls.

A simpler semantics is one of the main motivations behind Prela [1], and despite its simplicity, we now know it’s powerful enough to express thousands of queries in the wild [2], as well as run doom [3].

[1]: https://prela-lang.org/

[2]: https://github.com/remysucre/prela/tree/sqlstorm

[3]: https://github.com/remysucre/prela/tree/doom/