An introduction to Witch

A proof assistant is a software that helps a user find formal proofs to a problem or prove certain properties about their program. Thanks to proof assistants, numerous theorems have been proven, including the four color theorem. This theorem states that “given any separation of a plane into contiguous regions, producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color” [1].

Note that this theorem still has no proof created without a computer assistant. Several proof assistants exist, see f.i.: Agda, Coq, Isabelle/HOL. Proof assistants are powerful tools, but most of them are not user-friendly. They require a good knowledge of mathematics and computer science as well as experience with the chosen proof assistant. Moreover, in order to write a proof, users need to be well versed in the formal theory. This specialized knowledge forms a high barrier to entry that hinders the adoption of proof assistants. Different solutions have been proposed to increase the adoption of proof assistants (see f.i. lean forward).

The Juvix team (more details below) has been looking for different ways to lower the barrier of proof writing. Multiple solutions exist for proving theorems of varying fields (linear algebra, first-order logic, theories of real numbers, etc.). We decided to choose algebraic effects and handlers as it seemed that it would be an adequate solution to unify all automatic proof solutions under one programmable interface. Algebraic effects were introduced by Plotkin and Power as an algebraic equivalent of generic effects. Handlers were proposed later by Plotkin and Pretnar to handle exceptions algebraically. To learn more about algebraic effects and handlers, please consult this article.

By choosing algebraic effects and handlers, the Juvix team created the project Witch (named as reference to the software wizard). Thanks to Witch, users can program as they usually do and use the proof environment (a witch) as an effect to prove specific properties of their programs. Moreover, as the proof environment will be used as an effect, it allows combining different automated proof engines and proof styles.

This provides the user with a unified tool to apply different styles to different problems, allowing different proof styles to be constructed. Have a look at the simplified example below:

In the above example, a user would like to prove the commutativity of addition for natural numbers (1st column of the regular Haskell-style code) and the associativity of list concatenation (2nd column of the regular Haskell-style code). For that purpose, three main effects will be used: Solver, Proof Search, and Tactics, represented respectively by their operations solve, search, and tactic. This example shows that users will be able to combine different strategies (automated solvers, tactics, proof search, etc.) naturally, in order to prove theorems.

Witch is being implemented as part of the compiler for the Juvix programming language. Juvix is a dependent-linearly-typed core language specially developed to write safe smart contracts. With Witch, users’ gains will be twofold: composability of many strategies and knowledge sharing via a shared interface under handlers.

To learn more about Witch, please follow this link. To learn more about Juvix, visit this website.

References

[1] Four colour theorem, accessed: 2020-11-03.

[2] Witch article

Metastate has ceased its activities on the 31st of January 2021. The team members have joined a new company and working on a new project. If you're interested in programming language theory, functional programming, type theory, formal verification, or compiler engineering positions, check out the open positions at Heliax.

If you have any feedback or questions on this article, please do not hesitate to contact us: hello@heliax.dev.