- Create a language that allows the user to construct proofs (i.e sequences of transformations from a given input to output)
- How should the proof/program be formatted? Generate LaTeX?
- How should the rules be formatted? Generate LaTeX?
- How can an inductive proof be given? base case / inductive step / ???
- Can the computation of proofs be optimised? e.g. by combining several steps int one transformation
- Can parts of the proof be reformatted as theorems/lemmas?