# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1347285171 -7200
# Node ID 55d74481379b1747ffd3fc6792e98808510fdbd4
# Parent  a9cee7518066bcc417d7b44798bc391fb08c95e2# Parent  7e4deb0d71a9cc272ccbe1c392420b6c15e21efd
merged

diff -r a9cee7518066 -r 55d74481379b doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex
--- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 21:18:00 2012 +0200
+++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Mon Sep 10 15:52:51 2012 +0200
@@ -1626,9 +1626,70 @@
 % 
 % fehlermeldungen! TODO
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
+
 \section{Conclusion}\label{conclusion}
+This paper gives a first experience report about programming with a
+TP-based programming language.
 
-TODO
+\medskip A brief re-introduction of the novel kind of programming
+language by example of the {\sisac}-prototype makes the paper
+self-contained. The main section describes all the main concepts
+involved in TP-based programming and all the sub-tasks concerning
+respective implementation: mechanisation of mathematics and domain
+modelling, implementation of term rewriting systems for the
+rewriting-engine, formal (implicit) specification of the problem to be
+(explicitly) described by the program, implement the many components
+required for Lucas-Interpretation and finally implementation of the
+program itself.
+
+The many concepts and sub-tasks involved in programming require a
+comprehensive workflow; first experiences with the workflow as
+supported by the present prototype are described as well: Isabelle +
+Isar + jEdit provide appropriate components for establishing an
+efficient development environment integrating computation and
+deduction. However, the present state of the prototype is far off a
+state appropriate for wide-spread use: the prototype of the program
+language lacks expressiveness and elegance, the prototype of the
+development environment is hardly usable: error messages still address
+the developer of the prototype's interpreter rather than the
+application programmer, implementation of the many settings for the
+Lucas-Interpreter is cumbersome.
+
+From these experiences a successful proof of concept can be concluded:
+programming arbitrary problems from engineering sciences is possible,
+in principle even in the prototype. Furthermore the experiences allow
+to conclude detailed requirements for further development:
+\begin{itemize}
+\item Clarify underlying logics such that programming is smoothly
+integrated with verification of the program; the post-condition should
+be proved more or less automatically, otherwise working engineers
+would not encounter such programming.
+\item Combine the prototype's programming language with Isabelle's
+powerful function package and probably with more of SML's
+pattern-matching features; include parallel execution on multi-core
+machines into the language desing.
+\item Extend the prototype's Lucas-Interpreter such that it also
+handles functions defined by use of Isabelle's functions package; and
+generalize Isabelle's code generator such that efficient code for the
+whole of the defined programming language can be generated (for
+multi-core machines).
+\item Develop an efficient development environment with
+integration of programming and proving, with management not only of
+Isabelle theories, but also of large collections of specifications and
+of programs.
+\end{itemize} 
+Provided successful accomplishment, these points provide distinguished
+components for virtual workbenches appealing to practictioner of
+engineering in the near future.
+
+\medskip And all programming with a TP-based language will
+subsequently create interactive tutoring as a side-effect:
+Lucas-Interpretation not only provides an interactive programming
+environment, Lucas-Interpretation also can provide TP-based services
+for a flexible dialog component with adaptive user guidance for
+independent and inquiry-based learning.
+
 
 \bibliographystyle{alpha}
 \bibliography{references}