Despite the deficiencies in PGIP and complexities of Isabelle, I believe that this is the best direction for further research into theorem proving interfaces. Defining a clean interface between proof assistant and proof interface will have long term benefits for both developers and ultimately users.
I hope that Igloo has provided some insight into features sought by theorem prover interface developers, while also being designed to be simple enough to encourage non-experts to consider making use of formal theorem proving.
|
|
|