One post tagged with "internal error"

In this blog post, I propose to make you discover how we deal with internal errors and show that they do not occur while running the protocol! I will first give you a glimpse of the so-called error monad (but without going into the details of the notion of monad 🙂). You actually don't need to have any knowledge of monads in computer programming or elsewhere to read this article: we will take them step by step. But if you are already familiar on them, you can skim through the first parts of this post and have a look at the monadic let ... ins we use and how we articulate them with validity predicates. We conclude by giving a first glimpse at how we use these validity predicates to manually specify information which is lost during the automatic translation from OCaml to Coq.