Ruby Extension Library Verified using Coq Proof-assistant

on YouTube ↗44m

" summary

Generates C from Coq via a custom plugin and produces a working Ruby extension (html_escape) used from Ruby; Coq proofs show functional correctness (fast_power equals naive power) and prove safety properties like verified absence of overflows for inputs within specified bounds. Plugin emits Coq-generated C but the plugin itself is not machine-verified. Implementation includes SSE m128 support and microbenchmarks: the SSE path wins up to ~25% escapable characters and the generated extension runs correctly when loaded.

AI-written summary · about

" chapters (11)

1. 0:00Introduction to talk
2. 1:48What is Coq proof assistant
3. 3:20Verifying Ruby extensions with Coq
4. 8:20Implementing fast power in Coq
5. 12:30Curry-Howard correspondence
6. 20:40Verifying HTML escape function
7. 27:30Using SSE for faster HTML escape
8. 31:34Generating verified C code
9. 32:42Benchmarking performance
10. 34:31Why learn Coq
11. 38:50Q&A

" related talks

• 35mRuby’s C Extension Problem and How We're Solving ItChris Seaton · RubyConf 2016
• 46mTowards a Ruby compilerCaleb Clausen · RubyConf 2009
• 33mFuzzing Ruby and C ExtensionsClaudio Contin · BSidesSF 2018
• 24mThe State of C Extensions: Alive and Well, so Learn to DealSam Rawlins · MountainWest RubyConf 2011
• 46mAvoiding Pitfalls in C ExtensionsPaul Brannan · RubyConf 2007
• 45mFuture of RubyVMKoichi Sasada · RubyConf 2008
• 50mUsing C to Tune Your Ruby (or Rails) ApplicationJared Richardson · Ruby Hoedown 2007
• 27mGoing PostelScott Werner · RubyConf 2024