-Huge libraries of formal mathematics have been developed, and backward
-compatibility is a really time consuming task. \\
-A real-life example in the history of \MATITA{} was the reordering of
-goals opened by a tactic application. We noticed that some tactics
-were not opening goals in the expected order. In particular the
-\texttt{elim} tactic on a term of an inductive type with constructors
-$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
-\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
-but some theorems about integers were there. The inductive type of
-$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
-induction proofs on this type where written without tacticals and,
-obviously, considering the three induction cases in the wrong order.
-Fixing the behavior of the tactic broke the library and two days of
-work were needed to make it compile again. The whole time was spent in
-finding the list of tactics used to prove the third induction case and
-swap it with the list of tactics used to prove the second case. If
-the proofs was structured with the branch tactical this task could
-have been done automatically.
-
-From this experience we learned that the use of tacticals for
-structuring proofs gives some help but may have some drawbacks in
-proof script readability. We must highlight that proof scripts
-readability is poor by itself, but in conjunction with tacticals it
-can be nearly impossible. The main cause is the fact that in proof
-scripts there is no trace of what you are working on. It is not rare
-for two different theorems to have the same proof script (while the
-proof is completely different).\\
-Bad readability is not a big deal for the user while he is
-constructing the proof, but is considerably a problem when he tries to
-reread what he did or when he shows his work to someone else. The
-workaround commonly used to read a script is to execute it again
-step-by-step, so that you can see the proof goal changing and you can
-follow the proof steps. This works fine until you reach a tactical. A
-compound statement, made by some basic tactics glued with tacticals,
-is executed in a single step, while it obviously performs lot of proof
-steps. In the fist example of the previous section the whole branch
-over the two goals (respectively the left and right part of the logic
-and) result in a single step of execution. The workaround does not work
-anymore unless you de-structure on the fly the proof, putting some
-``\texttt{.}'' where you want the system to stop.\\
-
-Now we can understand the tradeoff between script readability and
-proof structuring with tacticals. Using tacticals helps in maintaining
-scripts, but makes it really hard to read them again, cause of the way
-they are executed.
-
-\MATITA{} uses a language of tactics and tacticals, but tries to avoid
-this tradeoff, alluring the user to write structured proof without
-making it impossible to read them again.
+%Huge libraries of formal mathematics have been developed, and backward
+%compatibility is a really time consuming task. \\
+%A real-life example in the history of \MATITA{} was the reordering of
+%goals opened by a tactic application. We noticed that some tactics
+%were not opening goals in the expected order. In particular the
+%\texttt{elim} tactic on a term of an inductive type with constructors
+%$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
+%\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
+%but some theorems about integers were there. The inductive type of
+%$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
+%induction proofs on this type where written without tacticals and,
+%obviously, considering the three induction cases in the wrong order.
+%Fixing the behavior of the tactic broke the library and two days of
+%work were needed to make it compile again. The whole time was spent in
+%finding the list of tactics used to prove the third induction case and
+%swap it with the list of tactics used to prove the second case. If
+%the proofs was structured with the branch tactical this task could
+%have been done automatically.
+%
+%From this experience we learned that the use of tacticals for
+%structuring proofs gives some help but may have some drawbacks in
+%proof script readability.
+
+Tacticals are not only used to make scripts shorter by factoring out
+common cases and repeating commands. They are a primary way of making
+scripts more mainteable. Moreover, they also have the well-known
+role of structuring the proof.
+
+However, authoring a proof structured with tacticals is annoying.
+Consider for example a proof by induction, and imagine you
+are using one of the state of the art graphical interfaces for proof assistant
+like Proof General. After applying the induction principle you have to choose:
+immediately structure the proof or postpone the structuring.
+If you decide for the former you have to apply the branching tactical and write
+at once tactics for all the cases. Since the user does not even know the
+generated goals yet, he can only replace all the cases with the identity
+tactic and execute the command, just to receive feedback on the first
+goal. Then he has to go one step back to replace the first identity
+tactic with the wanted one and repeat the process until all the
+branches are closed.
+
+One could imagine that a structured script is simpler to understand.
+This is not the case.
+A proof script, being not declarative, is not meant to be read.
+However, the user has the need of explaining it to others.
+This is achieved by interactively re-playing the script to show each
+intermediate proof status. Tacticals make this operation uncomfortable.
+Indeed, a tactical is executed atomically, while it is obvious that it
+performs lot of smaller steps we are interested in.
+To show the intermediate steps, the proof must be de-structured on the
+fly, for example replacing ``\texttt{;}'' with ``\texttt{.}'' where
+possible.\\
+
+%Proof scripts
+%readability is poor by itself, but in conjunction with tacticals it
+%can be nearly impossible. The main cause is the fact that in proof
+%scripts there is no trace of what you are working on. It is not rare
+%for two different theorems to have the same proof script.\\
+%Bad readability is not a big deal for the user while he is
+%constructing the proof, but is considerably a problem when he tries to
+%reread what he did or when he shows his work to someone else. The
+%workaround commonly used to read a script is to execute it again
+%step-by-step, so that you can see the proof goal changing and you can
+%follow the proof steps. This works fine until you reach a tactical. A
+%compound statement, made by some basic tactics glued with tacticals,
+%is executed in a single step, while it obviously performs lot of proof
+%steps. In the fist example of the previous section the whole branch
+%over the two goals (respectively the left and right part of the logic
+%and) result in a single step of execution. The workaround does not work
+%anymore unless you de-structure on the fly the proof, putting some
+%``\texttt{.}'' where you want the system to stop.\\
+
+%Now we can understand the tradeoff between script readability and
+%proof structuring with tacticals. Using tacticals helps in maintaining
+%scripts, but makes it really hard to read them again, cause of the way
+%they are executed.
+
+\MATITA{} has a peculiar tacticals implementation that provides the
+same benefits as classical tacticals, while not burdening the user
+during proof authoring and re-playing.
+
+%\MATITA{} uses a language of tactics and tacticals, but tries to avoid
+%this tradeoff, alluring the user to write structured proof without
+%making it impossible to read them again.