The Ethical Compiler: Addressing the Is-Ought Gap in Compilation
summary
Paper argues that compilers should be ethical not merely correct and presents six metaethical dictums: let programmers express what ought to hold, ensure anything that ought to hold is possible, and preserve intent through compilation. Concrete fixes include adding language annotations (Rust/rock examples), new semantics and keywords to make dead stores observable (C example), dependent-type checking to remove WebAssembly bounds checks, region systems to prevent heap-cycles that break termination, and a rule: never infer ought from is.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 4:20Ethics and is-ought gap in compilation
- 13:10Ethical vs traditional correctness
- 15:01Six metaethical dictums
- 16:03Programmer intent via types
- 20:13Types for ethical axioms
- 23:11Preserving intent in linking
- 24:14Challenges in intent preservation
- 28:49Truth versus intent in design
- 33:46Ethical error reporting
- 37:41Ethical compilation summary
- 38:30Q&A
related talks
22mCompilers should get over themselves and respect semantic dependencies!
53mLocknote: How Badly Do We Want Correct Compilers?
30mCalculating Compilers for Concurrency
01h 06mVerifying a compiler through equational means
39mAsk Me Anything with Alex Aiken
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
06mReasoning with function signatures
39mIs Go A Good Language to Build Compilers?