Generative Programming and Verification
summary
A <500-line SQL engine is implemented in Scala that starts as a relational-algebra interpreter and, via lightweight modular staging and Scala’s type system, generates low-level code and even C output; this pipeline yields microbenchmarks that beat commercial and open-source databases and gives a <500-line SQL engine with 20x speedup on staged matrix code. The workflow generates verification annotations so generated C parsers and routines are provably safe — e.g. a staged HTTP parser is verified free of memory and overflow errors.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:45Scala
- 2:05Performance
- 3:07The problem with abstraction
- 4:48Staging
- 6:31Matrix example
- 7:57Code in Scala
- 8:26DSL Implementation
- 14:58Code Generation
- 20:04Patterns
- 23:14Case Study
- 24:25Generic Support Library
- 28:29Pricing and Validation
- 28:56Parsing
- 31:10Security
- 33:24Type Classes
- 35:53Summary
- 37:10Learning more
related talks
30mFormal verification of Scala programs with Stainless
19mAutomated Verification of Fundamental Algebraic Laws
40mSafe Coding with LLMs - Verifiable Scala Silver Bullet
21mReasonable Scala Compiler
32mPRETTY LITTLE COMPILERS
14mMulti-stage Programming in the Large with Staged Classes
16mCompiling Symbolic Execution with Staging and Algebraic Effects
01h 09mCompilers are Databases