Thorium: Verifiable, Dynamic, Reactive Software
summary
A new declarative language called Thorium language models reactive programs as named reactors that can be swapped by module substitution and aims for glitch-free semantics. Verification compiles bounded traces to constraints solved by the Z3 SMT solver to produce counterexample traces. Prototype proves safety properties but hits severe performance limits—a simple three-stage configured pipeline explodes solver time (runs take hours), optimistic semantics collapse liveness, and subreactor explosion requires heuristics or bounds.
AI-written summary · about
chapters (12)
- 0:00Introduction to Thorium
- 3:13Glitch-free reactive system goals
- 7:31Thorium rules and terms
- 13:11Bounded model checking with Z3
- 18:56Interpreting counterexamples
- 21:24Performance challenges
- 27:28Optimizing SMT solver
- 30:33Thorium future plans
- 33:26Q&A
- 34:08Q&A on SMT solver
- 35:58Q&A on metric temporal logic
- 38:07Q&A on runtime
related talks
28mReactive Programming on the Bare Metal:A Formal Model for a Low-Level Reactive Virtual Machin
53mReactive Mythbusters With Reactor
29mThe Essence of Reactivity
47mReactive Programming - Royal Road or Wrong Turn?
27mReactive: Understand and Embrace
51mReactor 3, the reactive foundation for Java 8 (and Spring 5)
01h 10mReactor in Action - Simon Baslé, Victor Grazi
55mFlight of the Flux: A look at Reactor execution model