Ruby Extension Library Verified using Coq Proof-assistant

Ruby extension library is written in C. C is great because it is fast and easy to access low-level features of OS and CPU. However it is dangerous and error-prone: it is difficult to avoid failures such as integer overflow and buffer overrun. We explain a method to generate C functions verified using Coq proof-assistant with Coq plugins we developed. We can verify safety (absence of failures) and correctness (functions works as expected) in Coq. The generated functions can be used in Ruby extension library. This provides a way to develop trustful Ruby extension library. Supplement material: https://github.com/akr/coq-html-escape