You may have read our recent post discussing our involvement in the Gospel Project. In today's follow-up post, we will focus on Ortac, a tool we have been developing at Tarides as part of the Gospel Project. What is Ortac? Ortac aims to give OCaml programmers easy access to dynamic formal verification, also known as specification-driven testing. At its core, it translates computable Gospel terms into equivalent OCaml expressions. Different Ortac modes can then use these translations to genera...
