In the first part of our series about formal verification, we discuss the roots of formal verification in fields such as mathematical logic and theoretical computer science.
In the previous post, we briefly introduced the reader to dependently typed programming and theorem proving in Agda. Now we present an empty type to work with constructive negation. We discuss Marko…