Skip to content
Joshua Pratt edited this page Sep 30, 2018 · 2 revisions

Welcome to the HTriple wiki!

HTriple is an attempt to write a DSL and set of automated solvers that allow software developers to write arbitrary proofs about their algorithms using a mix of static and runtime checks.

It is based on Hoare Logic, a formal system for correctness proofs but is intended to support arbitrary extensions such as Type systems, Effect systems and Separation logics.

Clone this wiki locally