Interactive Theorem Proving

Interactive theorem proving such as one provided by Agda is so empowering. The help provided by the compiler while interactively developing a proof is invaluable. Types guide you to a solution at every single step.

Leave a Reply

Your email address will not be published. Required fields are marked *

IMPORTANT! To be able to proceed, you need to solve the following simple math (so we know that you are a human) :-)

What is (1 + 3] + 200?
Please leave these three fields as-is: