1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Sun Sep 09 21:12:49 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Mon Sep 10 15:52:44 2012 +0200
1.3 @@ -1573,9 +1573,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}