Executable Proofs for 15-150

Initially, proof assistants were targeted toward professional mathematicians, but interest has been rising regarding their potential use in undergraduate education. However, usability is still a major concern when it comes to introducing students to such systems. In this paper, we present Silkie, a system with an intuitive interface that would allow instructors to use proof assistants in undergraduate computer science education. It is built using SMLtoCoq, which translates SML code into Coq definitions, and an adapted version of JSCoq, a web-based implementation of the Coq theorem prover. Silkie is especially useful in courses that require students to write code and formally prove its correctness. Students can upload SML code into Silkie, and see the corresponding Coq definitions, which they can then use to prove properties about.  The proof tactics were modified such that "simple'' steps that are typically expected from students need to be explicit, and the language resembles more what would be written on paper. Moreover, the interface will structure the proof script depending on the commands used, such that the hierarchy of each proof part is clear.