1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 21:18:00 2012 +0200
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Mon Sep 10 15:52:51 2012 +0200
     1.3 @@ -1626,9 +1626,70 @@
     1.4  % 
     1.5  % fehlermeldungen! TODO
     1.6  
     1.7 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{verbatim}
     1.8 +
     1.9  \section{Conclusion}\label{conclusion}
    1.10 +This paper gives a first experience report about programming with a
    1.11 +TP-based programming language.
    1.12  
    1.13 -TODO
    1.14 +\medskip A brief re-introduction of the novel kind of programming
    1.15 +language by example of the {\sisac}-prototype makes the paper
    1.16 +self-contained. The main section describes all the main concepts
    1.17 +involved in TP-based programming and all the sub-tasks concerning
    1.18 +respective implementation: mechanisation of mathematics and domain
    1.19 +modelling, implementation of term rewriting systems for the
    1.20 +rewriting-engine, formal (implicit) specification of the problem to be
    1.21 +(explicitly) described by the program, implement the many components
    1.22 +required for Lucas-Interpretation and finally implementation of the
    1.23 +program itself.
    1.24 +
    1.25 +The many concepts and sub-tasks involved in programming require a
    1.26 +comprehensive workflow; first experiences with the workflow as
    1.27 +supported by the present prototype are described as well: Isabelle +
    1.28 +Isar + jEdit provide appropriate components for establishing an
    1.29 +efficient development environment integrating computation and
    1.30 +deduction. However, the present state of the prototype is far off a
    1.31 +state appropriate for wide-spread use: the prototype of the program
    1.32 +language lacks expressiveness and elegance, the prototype of the
    1.33 +development environment is hardly usable: error messages still address
    1.34 +the developer of the prototype's interpreter rather than the
    1.35 +application programmer, implementation of the many settings for the
    1.36 +Lucas-Interpreter is cumbersome.
    1.37 +
    1.38 +From these experiences a successful proof of concept can be concluded:
    1.39 +programming arbitrary problems from engineering sciences is possible,
    1.40 +in principle even in the prototype. Furthermore the experiences allow
    1.41 +to conclude detailed requirements for further development:
    1.42 +\begin{itemize}
    1.43 +\item Clarify underlying logics such that programming is smoothly
    1.44 +integrated with verification of the program; the post-condition should
    1.45 +be proved more or less automatically, otherwise working engineers
    1.46 +would not encounter such programming.
    1.47 +\item Combine the prototype's programming language with Isabelle's
    1.48 +powerful function package and probably with more of SML's
    1.49 +pattern-matching features; include parallel execution on multi-core
    1.50 +machines into the language desing.
    1.51 +\item Extend the prototype's Lucas-Interpreter such that it also
    1.52 +handles functions defined by use of Isabelle's functions package; and
    1.53 +generalize Isabelle's code generator such that efficient code for the
    1.54 +whole of the defined programming language can be generated (for
    1.55 +multi-core machines).
    1.56 +\item Develop an efficient development environment with
    1.57 +integration of programming and proving, with management not only of
    1.58 +Isabelle theories, but also of large collections of specifications and
    1.59 +of programs.
    1.60 +\end{itemize} 
    1.61 +Provided successful accomplishment, these points provide distinguished
    1.62 +components for virtual workbenches appealing to practictioner of
    1.63 +engineering in the near future.
    1.64 +
    1.65 +\medskip And all programming with a TP-based language will
    1.66 +subsequently create interactive tutoring as a side-effect:
    1.67 +Lucas-Interpretation not only provides an interactive programming
    1.68 +environment, Lucas-Interpretation also can provide TP-based services
    1.69 +for a flexible dialog component with adaptive user guidance for
    1.70 +independent and inquiry-based learning.
    1.71 +
    1.72  
    1.73  \bibliographystyle{alpha}
    1.74  \bibliography{references}