All the Languages Together
summary
Proposes that safe multi-language composition requires concrete annotations and compilers not vague promises: add linking types (e.g. linear types for ownership, purity annotations for termination) and use type-preserving and equivalence‑preserving compilation so low-level code carries the same specs. Demonstrations are research prototypes (Mulberry) targeting a richly typed WebAssembly and ongoing proofs of secure compilation; results are partial but show the checker/linker approach can catch cross‑language violations before runtime rather than after.
AI-written summary · about
chapters (15)
- 0:00Intro
- 1:24Multi-Language Software is Hard!
- 11:41Current State of PL Design
- 23:30Reasoning about Refactoring
- 26:04Is this Refactoring Correct?
- 27:44PureLang with Linking Types Extension PureLang
- 29:19Refactoring: Pure Inputs
- 29:58Refactoring: Stateful Inputs
- 31:00Minimal Annotation Burden
- 34:17Type-Preserving Compilation
- 38:43Cross-Language Type Errors
- 43:01Preserving Correctness of Refactoring
- 45:56Mulberry Project
- 48:22What about Untyped Languages?
- 50:01Takeaways
related talks
01h 04mWhat FP Can Learn From Formal Languages: Towards a Leaner Syntax
45mBack to Front and Beyond
21mEverything as Compiler
30mCompose All the Things
30mConcrete Syntax Metapatterns
46mCompilers, User Interfaces & the Rest of Us
01h 04mThe Magic Behind Optimizing Compilers: Static Program Analysis
04mLightning talk - Expressions of Change