Ask the expert - Thinking Mathematically Above The Code Level
summary
Argues that design must be written at a higher level than code and gives concrete practice: use TLA+ and its model checker to write precise specs so users need not read implementation, and to force teams to resolve contradictions before coding. Describes a real parser bug where informal rules about level checking (primes) prove nontrivial so a formal spec is written and translated straightforwardly into Java. Notes temporal logic is for liveness and that Azure teams use specs to catch design mismatches early.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:20Beyond the Code
- 1:21Thinking Above the Code
- 7:45Warf Hypothesis
- 8:14Effective Communication
- 8:42Favorite collaborators
- 11:18What are programmers missing out
- 13:12What can educators do
- 13:58Raising the level in a team setting
- 18:03Question from Hill Wayne
- 18:28Temporal Logic
- 23:16Advice for beginners
- 24:45Audience Question
- 27:01Final Question
related talks
15mThinking Hard is not Enough
53mSemantics-based program manipulation in the age of LLMs
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...
25mP4-SpecTec: A Language Mechanization Framework for P4
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
01h 13mDesigning distributed systems with TLA+
29mIntegrating Language Engineering into the Software Development Process
39mAsk Me Anything with Alex Aiken