-\begin{lstClean}[numbers=left,caption={The \gls{UI} and code for entering a person in \gls{ITASK}.},label={lst:enter_person}]
-:: Person = { name :: String, gender :: Gender, dateOfBirth :: Date }[+\label{lst:dt_fro}+]
-:: Gender = Male | Female | Other String[+\label{lst:dt_to}+]
-
-derive class iTask Person, Gender[+\label{lst:dt_derive}+]
-
-enterPerson :: Task Person
-enterPerson
- = Hint "Enter a person:" @>> enterInformation [][+\label{lst:task_ui}+]
- >>! \result->Hint "You Entered:" @>> viewInformation [] result[+\label{lst:task_comb}+]
-\end{lstClean}
-
-\subsection{\texorpdfstring{\Gls{MTASK}}{MTask}}
-This thesis uses \gls{ITASK} in conjunction with \gls{MTASK}, an innovative \gls{TOP} language designed for defining interactive systems for \gls{IOT} edge devices \citep{koopman_task-based_2018}.
-Where \gls{ITASK} abstracts away from details such as user interfaces, data storage, and persistent workflows, \gls{MTASK} offers abstractions for edge layer-specific details such as the heterogeneity of architectures, platforms and frameworks; peripheral access; multitasking; task scheduling; and energy consumption.
-It is written in \gls{CLEAN} as a multi-view \gls{EDSL} and hence there are multiple interpretations of the language of which the byte code compiler is the most relevant for this thesis.
-From the terms in the \gls{TOP} language, a very compact binary representation of the work that needs to be done is compiled.
-This specification is then sent to a device that runs the \gls{MTASK} \gls{RTS}, a domain-specific \gls{TOP} engine implemented as a feather-light domain-specific \gls{OS}.
-\Gls{MTASK} is seamlessly integrated with \gls{ITASK}, it allows the programmer to define all layers of an \gls{IOT} system from a single declarative specification.
-
-\todo[inline]{Is this example useful? I think it's too technical}
-\Cref{lst:intro_blink} shows an interactive \gls{MTASK}\slash{}\gls{ITASK} application for blinking \pgls{LED} on the microcontroller every user-specified interval.
-\Crefrange{lst:intro:itask_fro}{lst:intro:itask_to} show the \gls{ITASK} part.
-First a \gls{SDS} is defined to communicate the blinking interval, then the \gls{MTASK} is connected using \cleaninline{withDevice}.
-Once connected, the \cleaninline{intBlink} task is sent to the device (\cref{lst:intro_liftmtask}) and in parallel, the value of the interval \gls{SDS} can be updated using an editor (\cref{lst:intro_editor}).
-The \cleaninline{intBlink} task (\crefrange{lst:intro:mtask_fro}{lst:intro:mtask_to}) is the \gls{MTASK} part of the application that has its own tasks, \glspl{SDS}, and \gls{UOD}.
-This task first defines \gls{GPIO} pin 13 to be of the output type (\cref{lst:intro:declarePin}) followed by lifting the \gls{ITASK} \gls{SDS} to an \gls{MTASK} \gls{SDS} (\cref{lst:intro:liftsds}).
-The main expression of the program calls the \cleaninline{blink} function with the initial state.
-This function on \crefrange{lst:intro:blink_fro}{lst:intro:blink_to} first reads the interval \gls{SDS}, waits the specified delay, writes the state to the \gls{GPIO} pin and calls itself recursively using the inverse of the state.
-
-\begin{lstClean}[numbers=left,caption={\Gls{MTASK}\slash{}\gls{ITASK} interactive blinking.},label={lst:intro_blink}]
-interactiveBlink :: Task Int[+\label{lst:intro:itask_fro}+]
-interactiveBlink =
- withShared 500 \iInterval->[+\label{lst:intro_withshared}+]
- withDevice {TCPSettings | host = ..., port = ...} \dev->
- liftmTask (intBlink iInterval) dev[+\label{lst:intro_liftmtask}+]
- -|| Hint "Interval (ms)" @>> updateSharedInformation [] iInterval[+\label{lst:intro_editor}+][+\label{lst:intro:itask_to}+]
-
-intBlink :: Shared sds Int -> MTask v Int | mtask, liftsds v & RWShared sds[+\label{lst:intro:mtask_fro}+]
-intBlink iInterval =
- declarePin D13 PMOutput \d13->[+\label{lst:intro:declarePin}+]
- liftsds \mInterval=iInterval[+\label{lst:intro:liftsds}+]
- In fun \blink=(\st->[+\label{lst:intro:blink_fro}+]
- getSds mInterval >>=. \i->delay i
- >>|. writeD d13 st >>|. blink (Not st))[+\label{lst:intro:blink_to}+]
- In {main = blink true}[+\label{lst:intro:mtask_to}+]
-\end{lstClean}
-
-\subsection{Other \texorpdfstring{\glsxtrshort{TOP}}{TOP} languages}
-While \gls{ITASK} conceived \gls{TOP}, it is not the only \gls{TOP} language and engine.
-Some \gls{TOP} languages and systems arose from Master's and Bachelor's thesis projects (e.g.\ \textmu{}Task \citep{piers_task-oriented_2016} and LTasks \citep{van_gemert_task_2022}) or were created to solve a practical problem (e.g.\ Toppyt \citep{lijnse_toppyt_2022} and hTask \citep{lubbers_htask_2022}).
-Furthermore, \gls{TOPHAT} is a fully formally specified \gls{TOP} language designed to capture the essence of \gls{TOP} formally \citep{steenvoorden_tophat_2019}.
-It is also possible to translate \gls{TOPHAT} code to \gls{ITASK} to piggyback on the \gls{TOP} engine it offers \citep[\citesection{G.3}]{steenvoorden_tophat_2022}.
-
-\section{Contributions}\label{sec:contributions}
-This section provides a thorough overview of the relation to publications and the scientific contributions of the episodes and chapters.
+As an example, \cref{lst:todo,fig:todo} show the code and \gls{UI} for an interactive to-do list application.
+The user modifies a shared to-do list through an editor directly or using some predefined actions.
+Furthermore, in parallel, the length of the list is shown to demonstrate \glspl{SDS}.
+Using \gls{ITASK}, complex collaborations of users and tasks can be described on a high level.
+
+From the data type definitions (\cref{lst:todo_dt}), using generic programming (\cref{lst:todo_derive}), the \glspl{UI} for the data types are automatically generated.
+Then, using the parallel task combinator (\cleaninline{-\|\|}) the task for updating the to-dos (\cref{lst:todo_update}) and the task for viewing the length are combined (\cref{lst:todo_length}, shown as \emph{Length: 2} in the bottom of the image).
+This particular parallel combinator uses the result of the left-hand side task.
+Both tasks operate on the to-do \gls{SDS} (\cref{lst:todo_sds}).
+The task for updating the to-do list is an editor (\cref{lst:todo_editor}) combined using a step combinator (\crefrange{lst:todo_contfro}{lst:todo_contto}).
+The actions either change the value, sorting or clearing it, or terminate the task by returning the current value of the \gls{SDS}, visualised as three buttons on the bottom right of the \gls{UI}.
+Special combinators (e.g.\ \cleaninline{@>>} at \cref{lst:todo_ui}) are used to tweak the \gls{UI} to display informative labels.
+\todo[inline]{Zou je hier niet zeggen dat dit iTask programma de Presentation en Application layer uit Figure 1.1 maakt door dezelfde code in de browser en op de server te runnen en alle netwerkdingen te genereren? Dat is hier wel niet erg nodig. Maar geeft je wel het opstapje om in 1.4.2.\ te zeggen dat de edge devices die wij willen gebruiken dat niet kunnen. Deze paragraaf kan ook in 1.4.2.}
+
+\cleaninputlisting[float=,firstline=6,lastline=22,tabsize=3,numbers=left,caption={The code for a shared to-do list in \gls{ITASK}.},label={lst:todo}]{lst/sharedlist.icl}
+
+\begin{figure}
+ \centering
+ \includegraphics[width=\linewidth]{todo0g}
+ \caption{The \gls{UI} for the shared to-do list in \gls{ITASK}.}%
+ \label{fig:todo}
+\end{figure}
+
+\subsection{The mTask system}
+The work for \gls{IOT} edge devices can often be succinctly described by \gls{TOP} programs.
+Software on microcontrollers is usually composed of smaller basic tasks, are interactive, and share data with other components or the server.
+The \gls{ITASK} system seems an obvious candidate for bringing \gls{TOP} to \gls{IOT} edge devices.
+However, an \gls{ITASK} application contains many features that are not needed on \emph{edge devices} such as higher-order tasks, support for a distributed architecture, or a multi-user web server.
+\todo[inline]{Dat is op zich toch niet zo'n probleem. Een iTAsk server heeft ook geen GUI, maar wel alle iTask code om die te maken.
+Het feit dat dit niet hoeft op een edge device geeft je wel een van de handvatten om mTask in minder memory te runnen}
+Furthermore, \gls{IOT} edge devices are in general not powerful enough to run or interpret \gls{CLEAN}\slash\gls{ABC} code, they just lack the processor speed and memory.
+To bridge this gap, \gls{MTASK} is developed, a domain-specific \gls{TOP} system for \gls{IOT} edge devices that is integrated in \gls{ITASK} \citep{koopman_task-based_2018}.
+The \gls{ITASK} language abstracts away from details such as user interfaces, data storage, client-side platforms, and persistent workflows.
+On the other hand, \gls{MTASK} offers abstractions for edge layer-specific details such as the heterogeneity of architectures, platforms, and frameworks; peripheral access; task scheduling; and lowering energy consumption.
+
+The \gls{MTASK} system is seamlessly integrated with \gls{ITASK}.
+Tasks in \gls{MTASK} are integrated in such a way that they function as regular \gls{ITASK} tasks.
+Furthermore, \glspl{SDS} on the device can proxy \gls{ITASK} \glspl{SDS}.
+Using \gls{MTASK}, the programmer can define all layers of an \gls{IOT} system as a single declarative specification.
+The \gls{MTASK} language is written in \gls{CLEAN} as a multi-view \gls{EDSL} and hence there are multiple interpretations possible.
+This thesis mostly discusses the byte code compiler.
+From an \gls{MTASK} task constructed at run time, a compact binary representation of the work that needs to be done is compiled.
+And while the byte code for \gls{MTASK} is generated at run time, the type system of the host language \gls{CLEAN} prevents type errors in the generated code.
+This byte code is then sent to a device that running the \gls{MTASK} \gls{RTS}.
+This feather-light domain-specific \gls{OS} is written in portable \gls{C} with a minimal device specific interface and it executes the tasks using interpretation and rewriting.
+
+To illustrate \imtask{}, an example application is shown.
+The application is an interactive application for blinking \pgls{LED} on the microcontroller at a certain frequency that can be set and updated at run time.
+\Cref{lst:intro_blink,fig:intro_blink} show the \gls{ITASK} part of the code and a screenshot.
+Using \cleaninline{enterInformation}, the connection specification of the \gls{TCP} device is queried through a web editor (\cref{lst:intro_enterDevice,fig:intro_blink_dev}).
+\Cref{lst:intro_withshared} defines \pgls{SDS} to communicate the blinking interval between the server and the edge device.
+The \gls{MTASK} device is connected using \cleaninline{withDevice} at \cref{lst:intro_withdevice}.
+Once connected, the \cleaninline{intBlink} task is sent to the device (\cref{lst:intro_liftmtask}) and, in parallel, a web editor is shown that updates the value of the interval \gls{SDS} (\cref{lst:intro_editor,fig:intro_blink_int}).
+To allow terminating of the task, the \gls{ITASK} task ends with a sequential operation that returns a constant value when the button is pressed, making the task stable.
+\todo[inline]{foto device+led?}
+\todo[inline]{enterDevice nieuwe regel, globale func?}
+
+\cleaninputlisting[float={!ht},firstline=10,lastline=18,numbers=left,caption={The \gls{ITASK} code for the interactive blinking application.},label={lst:intro_blink}]{lst/blink.icl}
+
+\begin{figure}
+ \centering
+ \begin{subfigure}{.5\textwidth}
+ \centering
+ \includegraphics[width=.9\linewidth]{blink1g}
+ \caption{Device selection.}\label{fig:intro_blink_dev}
+ \end{subfigure}%
+ \begin{subfigure}{.5\textwidth}
+ \centering
+ \includegraphics[width=.9\linewidth]{blink2g}
+ \caption{Changing the interval.}\label{fig:intro_blink_int}
+ \end{subfigure}
+ \caption{The \gls{UI} for the interactive blink application in \gls{MTASK}.}%
+ \label{fig:intro_blink}
+\end{figure}
+
+The \cleaninline{intBlink} task (\cref{lst:intro_blink_mtask}) is the \gls{MTASK} part of the application.
+It blinks \pgls{LED} on the edge device with the delay that is dynamically adjustable by the user via an \gls{ITASK} editor in the browser.
+It has its own tasks, \glspl{SDS}, and \gls{UOD}.
+This task first defines \gls{GPIO} pin 13 to be of the output type (\cref{lst:intro:declarePin}).
+Then the \gls{ITASK} \gls{SDS} is lifted to an \gls{MTASK} \gls{SDS} (\cref{lst:intro:liftsds}), enabling the machinery to keep the \gls{SDS} in sync both on the device and the server.
+The main expression of the program calls the \cleaninline{blink} function with an initial state.
+This function on \crefrange{lst:intro:blink_fro}{lst:intro:blink_to} first reads the interval \gls{SDS}, waits the specified delay, writes the state to the \gls{GPIO} pin, and calls itself recursively using the inverse of the state in order to run continuously.
+The \cleaninline{>>\|.} operator denotes the sequencing of tasks in \gls{MTASK}.
+
+\cleaninputlisting[float={!ht},linerange={23-,25-33},numbers=left,caption={The \gls{MTASK} code for the interactive blinking application.},label={lst:intro_blink_mtask}]{lst/blink.icl} %chktex 8
+\todo[inline]{Meer wit rondom =jes, doornummeren?}
+
+\subsection{Other TOP languages}
+While \gls{ITASK} conceived \gls{TOP}, it is no longer the only \gls{TOP} system.
+Some \gls{TOP} languages were created to fill a gap encountered in practise.
+Toppyt \citep{lijnse_toppyt_2022} is a general purpose \gls{TOP} language written in \gls{PYTHON} used to host frameworks for modelling command \& control systems.
+The hTask system is a \gls{TOP} system written in \gls{HASKELL} used as a vessel for experimenting with asynchronous \glspl{SDS} \citep{lubbers_htask_2022}.
+Furthermore, some \gls{TOP} systems arose from Master's and Bachelor's thesis projects.
+For example, \textmu{}Task \citep{piers_task-oriented_2016}, a \gls{TOP} language for modelling non-interruptible embedded systems in \gls{HASKELL}, and LTasks \citep{van_gemert_task_2022}, a \gls{TOP} language written in the dynamically typed programming language Lua.
+Finally, there are \gls{TOP} languages with strong academic foundations.
+\Gls{TOPHAT} is a fully formally specified \gls{TOP} language designed to capture the essence of \gls{TOP} \citep{steenvoorden_tophat_2019}.
+Such a formal specification allows for symbolic execution, hint generation, but also the translation to \gls{ITASK} for actually performing the work \citep{steenvoorden_tophat_2022}.
+\Citeauthor{steenvoorden_tophat_2022} distinguishes two instruments for \gls{TOP}: \gls{TOP} languages and \gls{TOP} engines.
+The language is the \emph{formal} language for specifying interactive systems.
+The engine is the software or hardware that executes these specifications as a ready-for-work application.
+\todo[inline]{Noemen dat een vergelijkbare semantics voor mTask under construction is met een verwijzing naar de thesis van Elina?}
+
+\section{Contributions}%
+\label{sec:contributions}
+This section provides a thorough overview of the relation between the scientific publications and the contents of this thesis.