prela

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/

Here are some SQL queries from standard benchmarks rewritten in Prela: https://github.com/remysucre/prela/tree/cidr#queries This is in rust and we’re still tweaking the language, so the syntax is slightly different from the post.

At the bottom is the actual code for the "language", which is only 79 lines. I found it helpful to read it first and then go back to the article. (On my initial reading I was like, "okay, but what is a Rel?") https://github.com/remysucre/prela/blob/main/tutorial/prela....

Prela is an embedded query language based on Tarski's Algebra of Relations. Its queries are concise, clear, and fast. It is implemented by shallow embedding in a host programming language: Prela operators are regular functions in the host. The implementation follows continuation-passing style which compiles to efficient columnar execution.