Home

Welcome to the Tako wiki!

Tako (formerly known as HTriple) is an attempt to write a DSL and set of automated solvers that allow software developers to write arbitrary proofs inside their code that let them ensure correctness 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.