alt Hacker NewsI last touched formal verification methods 20 years ago. Back then, Coq had the capacity to automatically transform your proof into OCaml. I would have expected that this would have only gotten better with time.
I last touched formal verification methods 20 years ago. Back then, Coq had the capacity to automatically transform your proof into OCaml. I would have expected that this would have only gotten better with time.
It’s been renamed recently. Maybe a few times. I think it’s rocq now. [1]
[1] https://rocq-prover.org/docs