## Reading

For the nineteenth class, we will read
**Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers** [PDF] [DOI] by Lawrence C. Paulson and Jasmin Christian Blanchette.

Remember when we read about Metis? Metis alluded its use in **Sledgehammer**, a **very powerful proof automation procedure in Isabelle/HOL**. Now we get to see Sledgehammer!

Sledgehammer works by **flattening goals** in Isabelle/HOL's logic (a classical higher-order logic called HOL) into **first-order logic**, then invoking first-order procedures to dispatch those goals. Sledgehammer also **reconstructs lower-level proofs** in the end, so that the resulting proof does not always rely on calls to Sledgehammer. (I am not sure to what degree proof reconstruction is used in practice, relative to keeping calls to Sledgehammer in the code.)

Probably the coolest thing about Sledgehammer is that **people actually use it**. That's impressive, because often one of the hardest problems of building powerful tools and automation is getting people to use it---that is, **adoption**. This paper focuses on the design decisions that contributed to adoption, at least in the authors' views.

Sledgehammer has seen a number of implementations in proof assistants other than Isabelle/HOL, including in Coq. But Sledgehammer remains immensely popular, while some of these other tools have not really taken off. The reasons for this are hard to pin down---and worthy of discussion.

You can find a reading guide and the discussion questions below.

Please note that **this is due the morning before class**, so that we can discuss it in person. And **please install the artifact before Thursday's class**.