Generative Programming and Verification
I will illustrate the promise of generative programming — writing expressive high-level programs that generate fast low-level code at runtime — with a small (<500 lines of code) SQL query engine that outperforms commercial and open source database systems. The key ingredient is a native interpreter for relational algebra operations, which we turn into a fast compiler with the help of the Scala type system. I will build the SQL engine step-by-step, focusing on generative programming patterns. Finally, I will touch upon verifying properties (e.g. no memory nor overflow errors, check contracts) of the low-level generated code, so that it is not only fast but also secure using a high-level, fast and safe HTTP parser as an example.
Nada Amin is a post-doctoral researcher at TU Darmstadt and before that, was a member of the Scala team at EPFL. She has contributed to Clojure’s core.logic and Google’s Closure compiler. She’s loved helping others learn to program ever since tutoring SICP as an undergraduate lab assistant at MIT.