Comment by remywang

3 hours ago

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/

2 comments

remywang

rrr_oh_man 2 hours ago

> In general, the spec must be human readable, and I believe to achieve that we must do away with SQL

Eh. Carthago delenda est? Why?

disgruntledphd2 35 minutes ago

Yeah, that's the most impractical part of the original post.
Like, SQL was around before I was born, and barring the immanence of the Machine God (and potentially even then), will be around long after I die (unless civilisation collapses, I guess).