Could a Machine ever write tests for our code
summary
Prototype RubyCorrect applies extended static checking via RubyESC (translating Ruby to Boogie and using Z3) and generates tests with symbolic execution via RubyCasGen (Myra → KSYM/KSAN). The system proves simple contracts, finds violations (Fibonacci example breaks when FIB(n-3) violates preconditions), and auto-generates concrete test inputs up to loop/recursion bounds (~3–4 levels), producing cases for n=0,2,3,4 while skipping redundant n=1. Major limits: heavy type annotations, incomplete stdlib specs, eval/dynamic code, and gaps in string/multiple-signature support.
AI-written summary · about
chapters (9)
- 0:00Introduction to verification
- 1:26Formal verification overview
- 2:52Extended static checking
- 7:22Under the hood of Ruby ESC
- 11:01Ruby to Boogie translation
- 16:11Limitations of Ruby ESC
- 18:40Symbolic execution
- 24:11Ruby Case Gen implementation
- 29:11Future improvements and Q&A
