Animated logic: Correct functional conversion to conjunctive normal form

Computational Logic is "the calculus of Computer Science" and is an essential field of this area. Courses on this subject are usually either too informal (only providing pseudo-code specifications) or overly formal (merely presenting rigorous mathematical definitions) when describing algorithms. In either case, there is an emphasis on paper-and-pencil definitions and proofs rather than on computational approaches. It is seldom the case where these courses present executable code, even if the pedagogical advantages of using tools are well known. In this paper, we present an approach to obtain formally verified implementations of classical Computational Logic algorithms. The chosen tool for this approach is the Why3 platform since it allows implementing functions very close to their mathematical definitions, as well as it concedes a high degree of automation in the verification process. As proof of concept, we implement and prove the conversion algorithms from propositional formulae to conjunctive normal form. We apply our proposal on two variants of the algorithm: one in direct-style and another with an explicit stack structure. Being both first-order, Why3 processes the proofs straightforwardly.