-
-
Notifications
You must be signed in to change notification settings - Fork 1
Home
Joshua Pratt edited this page Aug 4, 2019
·
2 revisions
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.