Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
summary
Etylizer, a static checker built on set-theoretic types, analyzes five years of student Erlang projects (≈4,600 functions after cleanup) and finds that only 14% carry specs yet 89% check clean and 11% (~500 functions) produce errors; 70% of reported issues are genuine type errors. Median check time is milliseconds (90% <10ms). A complex type-system refinement is replaced by a targeted syntactic rewrite that removes 43 false positives and keeps checks fast.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:45Set-theoretic types in Erlang
- 4:55Student expectations
- 6:39Student code corpus
- 9:12Unexpected results
- 12:25Exhaustiveness checking
- 13:48Type errors in Erlang
- 15:53False positives from if
- 18:41Rewriting if-expressions
- 20:47Why checkers missed issues
- 21:50Community split on if
- 22:32Summary
- 22:53Call to action
related talks
26mIs this really a refactoring? Automated equivalence checking for Erlang projects
38mA safer Elixir
18mSemantic-Type-Guided Bug Finding
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
47mThe Tension Between Expediency and Correctness
36mFunctional State Machines in Rust: Typestate and Newtype Patterns
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
44mDesigning code without types