Can a Programming Language Reason About Systems?
summary
Fault is a domain-specific language that compiles to SMT‑LIB2 and targets SMT solvers such as Z3 and other SMT backends, converting C‑style, programmer‑friendly syntax into single‑static‑assignment formulas. It implements stock‑flow models and state charts and adds probability and output formatting so models are readable. Examples include checking a 5,000‑page export regulation, analysing when a microservices architecture degrades, and solving Sudoku; the tool is experimental, open source on GitHub, and sometimes breaks.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 3:31How do experts think about systems
- 6:19What is a mental model
- 13:20Why write a programming language
- 15:52The math
- 19:29Stockflow model
- 21:38Fault model
- 24:24System Dynamics
- 28:32Visualizing the Model
- 30:54More Models
- 35:14State Charts
related talks
01h 00mAI Safety through Programming?
38mAutomatically Synthesising Programs that We Can Trust
33mCorrectness Too Cheap To Meter: Formal Verification and LLMs
16mA Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning(…)
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
46mBlueprints for a Universal Reasoning Machine
17mNeuro-Symbolic Proof Generation for Scaling Systems Software Verification
24mSubstrate engineering