Going Static, Gradually: Semantic Soundness and Telling the Truth at Scale
summary
Introduces Sound Dynamic as a semantics that makes Hack’s syntactic types correspond to semantic sets so types “don’t lie,” trading full deep checks for shallow runtime enforcement and a conservative rule around erased generics; codebase size is 10M+ lines. Adds like types (sugar for T|Dynamic) so invariants are preserved without invasive runtime changes. Rolled out via IDE hovers and error messages, integrated into linters and static tooling, and reduces unsafe lint-driven edits while keeping performance constraints.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:14Hack’s evolution from PHP
- 3:00Types that lie in Hack
- 7:32Runtime checks infeasible
- 8:37Sound Dynamic types
- 11:51Preserving invariants
- 13:58Balancing soundness and expressivity
- 16:48Impact at Meta
- 17:30Next 20 years for gradual typing
- 18:36Q&A
