Trust, But Verify (Programmatically)
summary
Claims that Elm’s type system cuts runtime errors with concrete numbers and examples: a company running ~100k lines of Elm reports zero runtime exceptions over three years; the Maybe type prevents nil errors by forcing explicit handling; a refactor from circles to polygons yields ~15 compiler errors, each fixed mechanically, and then the app compiles and works first try. Also shows practical tooling: property-based testing caught a microsecond vs millisecond timestamp truncation that unit tests would likely miss.
AI-written summary · about
chapters (14)
- 0:00Rocky Mountain Ruby
- 0:15Trust, But Verify (Programmatically)
- 1:24Let's talk about the future
- 1:46This stuff matters
- 4:33The future: programs helping us write programs
- 5:24The future is now
- 6:57Correctness measure: How many runtime exceptions?
- 8:25Program #1: the type system
- 18:15A bold claim
- 19:02A real-world example
- 20:51The big refactor
- 23:29Program #2: Property- based testing
- 24:33Properties for reverse
- 26:35Real-world example: JSON encoding/decoding
related talks
33mTrust, but Verify
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
32mVerifying Constant-Time Implementations
18mScalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)
05mTrust In Soft at embedded world North America 2026
32mDon’t let it crash: How we applied our security checks on Elixir code
01h 00mAI Safety through Programming?