Many hyperlinks are disabled.

Use anonymous login
to enable hyperlinks.

Overview

Comment: | Final draft of report. (Unless I think of something else to add...) |
---|---|

Downloads: | Tarball | ZIP archive | SQL archive |

Timelines: | family | ancestors | descendants | both | trunk |

Files: | files | file ages | folders |

SHA1: | 04f1cd06962f11344527d7f7f19230d82dce2a68 |

User & Date: | andy 2015-04-18 21:14:05 |

Context

2015-04-20
| ||

09:52 | Fixed a minor typo. Leaf check-in: adaef9d668 user: andy tags: trunk | |

2015-04-18
| ||

21:14 | Final draft of report. (Unless I think of something else to add...) check-in: 04f1cd0696 user: andy tags: trunk | |

19:48 | Penultimate draft of the report. After spell checking and such, this will become the final draft. check-in: 98924328ad user: andy tags: trunk | |

Changes

Changes to report/arend-report.pdf.

cannot compute difference between binary files

Changes to report/arend-report.tex.

319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 ... 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 ... 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 ... 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 ... 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 .... 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 .... 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 .... 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 .... 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 .... 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 .... 1902 1903 1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 .... 1959 1960 1961 1962 1963 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 .... 2026 2027 2028 2029 2030 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 |
smaller parts, lemmas can be used, like functions, to abstract out commonly-used subproofs, or to break down proofs that would otherwise be too large and unwieldy to understand. \item The lack of traditional negation eliminates some of the more-confusing elements of traditional logic programming. In particular, Arend has nothing corresponding to ``negation as failure''; it is not possible in Arend to know, in a computational sense, when a proposition $P$ fails. Thus reasoning in Arend is entirely about things that are known to be true, never about things that are assumed to be false. \end{itemize} Visually, Arend presents proofs as trees of subproofs. A proof in this presentation has the form \[ ................................................................................ will, if sufficiently ``smart'', be able to prove any theorem which a human with near-infinite patience could prove. Proofs produced by automated theorem provers are often quite lengthy, some stretching into the thousands-of-pages. Automated theorem provers must often employ sophisticated heuristics in their proof search algorithms, to avoid the exponential run times that would otherwise be required. \item \emph{Model checking} concerns the automatic checking of a given model against a formal specification. For example, given a state machine as a model of a computational system, we may wish to verify that the system never enters some particular set of error states. Since model checking is only tangentially related to our subject, we will not discuss it further. \item \emph{Proof assistants} aim to aid in the development and checking of formal proofs. While some systems only check proofs for completeness, more modern systems will typically also aid the user in the development of a proof. Recent examples include Coq \mcitep{Coq:manual}, Twelf \mcitep{pfenning1999system}, and Abella \mcitep{gacek08ijcar} Several element of Arend's design were influenced by Abella, most notably the use of a constructive two-level logic for describing and reasoning about systems. For a full history of the development of computer-assisted proof systems, see \mcitet{geuvers2009proof}. \item More recently, several systems have emerged which try to bridge the gap between traditional functional programming and theorem proving. Systems ................................................................................ is the same as saying that $t$ is a proof of $P$. Under this view, proof checking is the same as type checking. Arend is not directly based on the Curry-Howard isomorphism; although its proofs are terms, it does not check them by computing their types, since terms in Arend are untyped. Nonetheless, we believe that it should be possible to derive a consistent type system from Arend's reasoning logic, which would support this interpretation. Proof assistants that present a graphical interface are surprisingly rare. While graphical ``wrappers'' exist for some systems (for example, ProofWeb\link{http://prover.cs.ru.nl/login.php} for Coq), these were not a part of the design of their underlying systems. The only proof assistant of which we are aware which makes graphical interaction as much an integral feature as Arend is HLM \mcitep{reichelt2010types}. Like Arend, HLM encourages direct manipulation of in-progress proofs and is explicitly designed with that hope that it will ................................................................................ \begin{itemize} \item \mcitet{kadoda1999desirable} present the results of a survey on the desirable user-interface features in an educational proof assistant. One surprising result they describe is a positive correlation between both the interactivity of a system, and its ability to work with explicit proof trees, and the ``error-proneness'' of a system. This strikes us as a surprising result, as Arend is both interactive and works with explicit proof trees, and yet has virtually no error-proneness during the proof construction process, as users are limited strictly to those actions which will progress the proof in a valid way.\marginnote{It should be noted this author did not discover Kadoda's work until after Arend's design, with its emphasis on these features, was largely finalized.} However, several features which Kadoda describes as being ``highly'' desirable are present in Arend: its ................................................................................ \subsection{Reasoning logic} \newthought{Arend's reasoning logic} is closer to a full expression of first-order intuitionistic logic, with extensions to support proofs by single-induction. The inference rules defining the reasoning logic are presented in Figure \ref{reasoning-rules}. It supports rightward implication ($\rightarrow$), with the restriction that the premise cannot contain nested implications, only conjunctions, disjunctions, and atomic goals.\footnote{This restriction subsumes the \emph{stratification} restriction in Abella; stratification in some form is required to ensure monotonicity of the logic.} This implies that antecedents cannot contain implications, since they cannot be added by $\rightarrow_R$, and are not allowed in definitions in the specification logic. ................................................................................ \subsection{Proof representation} Informally, the content of a derivation is relatively simple: a tree of \textsc{-Left} and/or \textsc{-Right} rule applications, drawn from the rules of the reasoning logic in figure \ref{reasoning-rules}. In practice, a more detailed representation is required, one which, in particular, necessitates the use of \emph{explicit substitution}, rather than the implicit substitution that would result from naive use of (for example) the system unification in Prolog. For derivations purely derived from the specification language, explicit substitution is not required. This is because for any valid derivation of a proposition expressed in the specification language, the substitution is \emph{consistent} throughout the derivation tree; it is not possible for different ``branches'' to have different substitutions. (Disjunction may, of course, result in the generation of multiple distinct derivations, each with its own unifying substitution, but within any single derivation there is always a single consistent substitution.) ................................................................................ would need to have a conclusion $X = z \land X = s(x')$, which is already inconsistent, and actually impossible to express, because Horn clauses forbid such conjunctions as conclusions. Conversely, given the conclusion $X = z \lor X = s(x')$ we have the choice of which unification to use, and thus there is no inconsistency.} Because of this, each branch of a derivation must maintain its own substitution, applied to its goals as they are expanded. Proofs are represented as a term of the form \begin{verbatim} proof(Goal,Ctx,Subst,Proof) \end{verbatim} where \texttt{Goal} is the goal to be proved, \texttt{Ctx} is the list of antecedents (initially empty for most goals), \texttt{Subst} is the ................................................................................ various -Left rules of the reasoning logic. \item \texttt{trivial} --- Proves $\top$. \item \texttt{hole} --- Proves any goal, but represents an incomplete proof. \end{itemize} \subsection{Capture avoidance} The use of explicit substitution means that the proof-checker must also contend with another troublesome problem which Prolog conceals: avoiding \emph{accidental capture} when expanding a call to a goal. Consider the goal $\mathsf{nat}(X)$. We would expect this goal to succeed twice, first with the solution $X = z$. However, if we naively unify this goal with the head of the Nat-Succ rule we get the solution $X = s(X)$ which fails the occurs check. The problem is that $X$ as present in our goal is not the same variable as $X$ in the Nat-Succ rule. Variables in rule definitions are \emph{schematic}, their names should be ................................................................................ In this mode it can prove any proposition in the pure specification logic, and even a few that lie outside it; these extensions include: \begin{itemize} \item Simple implications: for example, $P -> P$ can be proved. \item Proofs involving $\bot$-Left, for example $\bot -> P$. \item Proofs involving limited use of other -Left rules. For example, $P \land Q -> P$ can be proved.\footnote{$P \land Q -> P$ produces an infinite sequence of proofs, because the list of premises, while properly speaking a set, is implemented as a list without duplicate removal, for efficiency reasons. Thus it is always possible to case on $P \land Q$, keep the original premise, and thus generate an infinite collection of $P$'s, each of which gives, theoretically, a distinct proof.} \end{itemize} More interestingly, \texttt{check} can be called with the \emph{goal} unbound and the proof bound, albeit for a very limited set of proofs. In this mode it will construct a proposition which is proved by the given proof. This behavior is not unexpected; by the Curry-Howard isomorphism proofs are ................................................................................ \end{lstlisting} with the (internal) restriction that the IH will never be used without explicit action on the part of the user. Lemmas, once proved, are represented similarly, as new program clauses, but requiring explicit use. A somewhat unfamiliar aspect of Arend's use of induction is how the inductive hypothesis is applied: ordinarily we would specify those premises of the current proof state which matched the corresponding premises of the IH (i.e., ``apply IH to $nat^\downarrow(X')$''); this would have the effect of introducing the IH, with the appropriate substitutions, as a new premise, where the assumption rule could then use it to prove the conclusion. Purely for user-interface reasons, we apply the IH by backchaining it against the current \emph{conclusion}, replacing the goal with the conjunction of the premises of the IH (again, with the appropriate substitutions). The user can then use the $\land$-R rule to split the proof into subproofs with atomic goals, each of which can be proved by the assumption rule. The inductive hypothesis is used within a proof by backchaining on the current goal, which must unify with the head of the IH. Recall that backchaining replaces the goal with its definition(s). Ordinarily the disjunction of ................................................................................ \item Currently Arend allows specification authors minimal influence on the \emph{user interface}; their power is limited to declaratively describing how certain predicates should be rendered as HTML. For more complex specifications, this is insufficient. As an example, classical logic can be specified in Arend with relative ease, via a predicate \texttt{solve}: \texttt{solve(C,G,T)} succeeds if the proposition $G$ evaluates to the truth value $T$ in context $C$. However, none of the familiar operations for manipulating the goal and premises can be used with this specification, as they are ``hidden'' inside the arguments to a predicate. A system allowing specification authors to highlight terms in various contexts as targets for user-manipulation would greatly extend the ease-of-use of the system when dealing with non-trivial specifications. \item Many proof assistants allow the user to create \emph{tacticals}, ``shortcuts'' through the proof process or alternate reasoning strategies. A cursory glance at the \emph{check/3} predicate at the heart of Arend's proof-checking algorithm will reveal a significant amount of similarity between the various cases: to apply a -Left or -Right rule, we apply some kind of transformation(s) to either one of the premises or the goal, and then recursively check zero or more of these transformed subproofs. Tacticals allow the user to specify these transformations themselves, in a way that enforces their consistency with the underlying logic. For some specifications, tacticals could significantly simplify the development of otherwise-tedious proofs, by concealing the irrelevant details. \item In a similar vein, Arend currently requires the user to proceed through ................................................................................ creating an ecosystem around student-created specifications, proofs, and lemmas, perhaps with collaboration features for multi-student use. \item Although we believe Arend's derivation-tree presentation of proofs has distinct advantages over the traditional paragraph format, there is no reason why an alternate user interface could not present proofs in that form, allowing users who feel more comfortable with a textual presentation to navigate their proofs in that way. Indeed, users could easily switch between the two presentations, and any other future presentations that might be added, even in the middle of a proof. Indeed, given the hierarchical structure of proofs, it is entirely possible that the two notations could be mixed within a single proof. The outer elements of a proof might be in paragraph form, while the individual cases were presented as derivations, or vice versa. ................................................................................ \emph{functional programs} and programming languages; we can state equivalences between expressions and then prove that two programs, or two classes of programs, are equivalent under those rules. Even more powerfully, if we wish to prove some property of an entire language, it is sufficient to show that the equivalences preserve that property. Although the additional of equational reasoning to Arend would give the system a marked increase in logical power, it would also correspondingly increase the complexity of its implementation and presentation. Equivalence rules require a different treatment of terms and variables from unification, and it is not entirely clear how the two will interact, logically. Equivalences over programs require careful handling of \emph{binders}, language constructs that introduce new (program) variables into scope. These variables are distinct from the logic variables, but can both contain, and be contained by, them. Although logics exist which provide support for reasoning about binding structures \mcitep{miller05tocl} their usage in proofs involves additional complexity that may be at odd with our goal of use in \emph{introductory} curriculum. \clearpage \section{Appendix I: Syntax of the Specification Logic} \label{sec:spec-syntax} \newcommand{\nterm}[1]{\mathop{\langle\text{#1}\rangle}} \newcommand{\sterm}[1]{\mathop{\text{\emph{#1}}}} |
| | | | | < | | > | | | > > > | | | | | | | | > | > | | | |
319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 ... 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 ... 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 ... 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 ... 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 .... 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 .... 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 .... 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 .... 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 .... 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 .... 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932 .... 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 .... 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 2051 2052 2053 2054 2055 |
smaller parts, lemmas can be used, like functions, to abstract out commonly-used subproofs, or to break down proofs that would otherwise be too large and unwieldy to understand. \item The lack of traditional negation eliminates some of the more-confusing elements of traditional logic programming. In particular, Arend has nothing corresponding to ``negation as failure''; it is not possible in Arend to know, in a computational sense, when a proposition $P$ fails. Thus, reasoning in Arend is entirely about things that are known to be true, never about things that are assumed to be false. \end{itemize} Visually, Arend presents proofs as trees of subproofs. A proof in this presentation has the form \[ ................................................................................ will, if sufficiently ``smart'', be able to prove any theorem which a human with near-infinite patience could prove. Proofs produced by automated theorem provers are often quite lengthy, some stretching into the thousands-of-pages. Automated theorem provers must often employ sophisticated heuristics in their proof search algorithms, to avoid the exponential run times that would otherwise be required. \item \emph{Model checkers} are concerned the automatic checking of a given model against a formal specification. For example, given a state machine as a model of a computational system, we may wish to verify that the system never enters some particular set of error states. Since model checking is only tangentially related to our subject, we will not discuss it further. \item \emph{Proof assistants} aim to aid in the development and checking of formal proofs. While some systems only check proofs for completeness, more modern systems will typically also aid the user in the development of a proof. Recent examples include Coq \mcitep{Coq:manual}, Twelf \mcitep{pfenning1999system}, and Abella \mcitep{gacek08ijcar}. Several element of Arend's design were influenced by Abella, most notably the use of a constructive two-level logic for describing and reasoning about systems. For a full history of the development of computer-assisted proof systems, see \mcitet{geuvers2009proof}. \item More recently, several systems have emerged which try to bridge the gap between traditional functional programming and theorem proving. Systems ................................................................................ is the same as saying that $t$ is a proof of $P$. Under this view, proof checking is the same as type checking. Arend is not directly based on the Curry-Howard isomorphism; although its proofs are terms, it does not check them by computing their types, since terms in Arend are untyped. Nonetheless, we believe that it should be possible to derive a consistent type system from Arend's reasoning logic, which would support this interpretation. Proof assistants that present a graphical interface are rare. While graphical ``wrappers'' exist for some systems (for example, ProofWeb\link{http://prover.cs.ru.nl/login.php} for Coq), these were not a part of the design of their underlying systems. The only proof assistant of which we are aware which makes graphical interaction as much an integral feature as Arend is HLM \mcitep{reichelt2010types}. Like Arend, HLM encourages direct manipulation of in-progress proofs and is explicitly designed with that hope that it will ................................................................................ \begin{itemize} \item \mcitet{kadoda1999desirable} present the results of a survey on the desirable user-interface features in an educational proof assistant. One surprising result they describe is a positive correlation between both the interactivity of a system, and its ability to work with explicit proof trees, and the ``error-proneness'' of a system. This strikes us as surprising, as Arend is both interactive and works with explicit proof trees, and yet has virtually no error-proneness during the proof construction process, as users are limited strictly to those actions which will progress the proof in a valid way.\marginnote{It should be noted this author did not discover Kadoda's work until after Arend's design, with its emphasis on these features, was largely finalized.} However, several features which Kadoda describes as being ``highly'' desirable are present in Arend: its ................................................................................ \subsection{Reasoning logic} \newthought{Arend's reasoning logic} is closer to a full expression of first-order intuitionistic logic, with extensions to support proofs by single-induction. The inference rules defining the reasoning logic are presented in Figure \ref{reasoning-rules}. It supports rightward implication ($\rightarrow$), with the restriction that the left-hand side cannot contain nested implications, only conjunctions, disjunctions, and atomic goals.\footnote{This restriction subsumes the \emph{stratification} restriction in Abella; stratification in some form is required to ensure monotonicity of the logic.} This implies that antecedents cannot contain implications, since they cannot be added by $\rightarrow_R$, and are not allowed in definitions in the specification logic. ................................................................................ \subsection{Proof representation} Informally, the content of a derivation is relatively simple: a tree of \textsc{-Left} and/or \textsc{-Right} rule applications, drawn from the rules of the reasoning logic in figure \ref{reasoning-rules}. In practice, a more detailed representation is required, one which, in particular, necessitates the use of \emph{manual substitution}, rather than the implicit substitution that would result from naive use of (for example) the system unification in Prolog. For derivations purely derived from the specification language, manual substitution is not required. This is because for any valid derivation of a proposition expressed in the specification language, the substitution is \emph{consistent} throughout the derivation tree; it is not possible for different ``branches'' to have different substitutions. (Disjunction may, of course, result in the generation of multiple distinct derivations, each with its own unifying substitution, but within any single derivation there is always a single consistent substitution.) ................................................................................ would need to have a conclusion $X = z \land X = s(x')$, which is already inconsistent, and actually impossible to express, because Horn clauses forbid such conjunctions as conclusions. Conversely, given the conclusion $X = z \lor X = s(x')$ we have the choice of which unification to use, and thus there is no inconsistency.} Because of this, each branch of a derivation must maintain its own substitution, applied to its goals as they are expanded. Thus, Arend contains facilities for implementing its own notion of logical variables, unifying terms containing these variables (producing a substitution object), and applying substitution objects to arbitrary terms. Proofs are represented as a term of the form \begin{verbatim} proof(Goal,Ctx,Subst,Proof) \end{verbatim} where \texttt{Goal} is the goal to be proved, \texttt{Ctx} is the list of antecedents (initially empty for most goals), \texttt{Subst} is the ................................................................................ various -Left rules of the reasoning logic. \item \texttt{trivial} --- Proves $\top$. \item \texttt{hole} --- Proves any goal, but represents an incomplete proof. \end{itemize} \subsection{Capture avoidance} The use of manual substitution means that the proof-checker must also contend with another troublesome problem which Prolog conceals: avoiding \emph{accidental capture} when expanding a call to a goal. Consider the goal $\mathsf{nat}(X)$. We would expect this goal to succeed twice, first with the solution $X = z$. However, if we naively unify this goal with the head of the Nat-Succ rule we get the solution $X = s(X)$ which fails the occurs check. The problem is that $X$ as present in our goal is not the same variable as $X$ in the Nat-Succ rule. Variables in rule definitions are \emph{schematic}, their names should be ................................................................................ In this mode it can prove any proposition in the pure specification logic, and even a few that lie outside it; these extensions include: \begin{itemize} \item Simple implications: for example, $P -> P$ can be proved. \item Proofs involving $\bot$-Left, for example $\bot -> P$. \item Proofs involving limited use of other -Left rules. For example, $P \land Q -> P$ can be proved.\footnote{$P \land Q -> P$ produces an infinite sequence of proofs, because the list of antecedents, while properly speaking a set, is implemented as a list without duplicate removal, for efficiency reasons. Thus it is always possible to case on $P \land Q$, keep the original antecedent, and thus generate an infinite collection of $P$'s, each of which gives, theoretically, a distinct proof.} \end{itemize} More interestingly, \texttt{check} can be called with the \emph{goal} unbound and the proof bound, albeit for a very limited set of proofs. In this mode it will construct a proposition which is proved by the given proof. This behavior is not unexpected; by the Curry-Howard isomorphism proofs are ................................................................................ \end{lstlisting} with the (internal) restriction that the IH will never be used without explicit action on the part of the user. Lemmas, once proved, are represented similarly, as new program clauses, but requiring explicit use. A somewhat unfamiliar aspect of Arend's use of induction is how the inductive hypothesis is applied: ordinarily we would specify those antecedents of the current proof state which matched the corresponding antecedents of the IH (i.e., ``apply IH to $nat^\downarrow(X')$''); this would have the effect of introducing the IH, with the appropriate substitutions, as a new antecedent, where the assumption rule could then use it to prove the conclusion. Purely for user-interface reasons, we apply the IH by backchaining it against the current \emph{conclusion}, replacing the goal with the conjunction of the antecedent of the IH (again, with the appropriate substitutions). The user can then use the $\land$-R rule to split the proof into subproofs with atomic goals, each of which can be proved by the assumption rule. The inductive hypothesis is used within a proof by backchaining on the current goal, which must unify with the head of the IH. Recall that backchaining replaces the goal with its definition(s). Ordinarily the disjunction of ................................................................................ \item Currently Arend allows specification authors minimal influence on the \emph{user interface}; their power is limited to declaratively describing how certain predicates should be rendered as HTML. For more complex specifications, this is insufficient. As an example, classical logic can be specified in Arend with relative ease, via a predicate \texttt{solve}: \texttt{solve(C,G,T)} succeeds if the proposition $G$ evaluates to the truth value $T$ in context $C$. However, none of the familiar operations for manipulating the consequent and antecedents can be used with this specification, as they are ``hidden'' inside the arguments to a predicate. A system allowing specification authors to highlight terms in various contexts as targets for user-manipulation would greatly extend the ease-of-use of the system when dealing with non-trivial specifications. \item Many proof assistants allow the user to create \emph{tacticals}, ``shortcuts'' through the proof process or alternate reasoning strategies. A cursory glance at the \emph{check/3} predicate at the heart of Arend's proof-checking algorithm will reveal a significant amount of similarity between the various cases: to apply a -Left or -Right rule, we apply some kind of transformation(s) to either one of the antecedents or the consequent, and then recursively check zero or more of these transformed subproofs. Tacticals allow the user to specify these transformations themselves, in a way that enforces their consistency with the underlying logic. For some specifications, tacticals could significantly simplify the development of otherwise-tedious proofs, by concealing the irrelevant details. \item In a similar vein, Arend currently requires the user to proceed through ................................................................................ creating an ecosystem around student-created specifications, proofs, and lemmas, perhaps with collaboration features for multi-student use. \item Although we believe Arend's derivation-tree presentation of proofs has distinct advantages over the traditional paragraph format, there is no reason why an alternate user interface could not present proofs in that form, allowing users who feel more comfortable with a textual presentation to navigate their proofs in that way. Users could easily switch between the two presentations, and any other future presentations that might be added, even in the middle of a proof. Indeed, given the hierarchical structure of proofs, it is entirely possible that the two notations could be mixed within a single proof. The outer elements of a proof might be in paragraph form, while the individual cases were presented as derivations, or vice versa. ................................................................................ \emph{functional programs} and programming languages; we can state equivalences between expressions and then prove that two programs, or two classes of programs, are equivalent under those rules. Even more powerfully, if we wish to prove some property of an entire language, it is sufficient to show that the equivalences preserve that property. Although the addition of equational reasoning to Arend would give the system a marked increase in logical power, it would also correspondingly increase the complexity of its implementation and presentation. Equivalence rules require a different treatment of terms and variables from unification, and it is not entirely clear how the two will interact, logically. Equivalences over programs require careful handling of \emph{binders}, language constructs that introduce new (program) variables into scope. These variables are distinct from the logic variables, but can both contain, and be contained by, them. Although logics exist which provide support for reasoning about binding structures \mcitep{miller05tocl} their usage in proofs involves additional complexity that may be at odds with our goal of use in \emph{introductory} curriculum. \clearpage \section{Appendix I: Syntax of the Specification Logic} \label{sec:spec-syntax} \newcommand{\nterm}[1]{\mathop{\langle\text{#1}\rangle}} \newcommand{\sterm}[1]{\mathop{\text{\emph{#1}}}} |