+ Future works comprise the implementation of new features and tutors, and
+ the embedding of the system in larger test cases. For instance, one
+ interesting case study would be interfacing a CAS as Maple to the
+ \hbugs{} broker, developing at the same time a tutor that implements the
+ Field tactic of Coq, which proves the equality of two expressions in an
+ abstract field by reducing both members to the same normal form. CASs can
+ produce several compact normal forms, which are particularly informative
+ to the user and that may suggest how to proceed in a proof. Unfortunately,
+ CASs do not
+ provide any certificate about the correctness of the simplification. On
+ the contrary, the Field tactic certifies the equality of two expressions,
+ but produces normal forms that are hardly a simplification of the original
+ formula. The benefits for the CAS would be obtained by using the Field tutor
+ to certify the CAS simplifications, proving that the Field normal form
+ of an expression is preserved by the simplification.
+ More advanced tutors could exploit the CAS to reduce the
+ goal to compact normal forms \cite{maplemodeforCoq}, making the Field tutor
+ certify the simplification according to the skeptical approach.
+