update stukje over ivory

diff --git a/acronyms.tex b/acronyms.tex
index 2481539..ac1d001 100644 (file)
--- a/acronyms.tex
+++ b/acronyms.tex
@@ -12,5 +12,4 @@
 \newacronym{TCP}{TCP}{Transmission Control Protocol}
 \newacronym{RFID}{RFID}{Radio-Frequency Identification}
 \newacronym{GPS}{GPS}{Global Positioning System}
-\newacronym{RTOS}{RTOS}{Real-Time Operating System}
 \newacronym{LCD}{LCD}{Liquid Crystal Display}

diff --git a/glossaries.tex b/glossaries.tex
index d05ca70..8b19444 100644 (file)
--- a/glossaries.tex
+++ b/glossaries.tex
@@ -12,9 +12,6 @@
 \newglossaryentry{Ivory}{name=Ivory,
        description={is a type-safe \gls{EDSL} designed to generate \gls{C}-code
        for high-assurance low-level systems}}
-\newglossaryentry{Tower}{name=Tower,
-       description={is a type-safe \gls{EDSL} similar to \gls{Ivory} designed to
-       generate code for \acrlong{RTOS}}}
 \newglossaryentry{Task}{name=Task,
        description={is the basic building block of a \acrshort{TOP} system}}
 \newglossaryentry{mTask}{name=mTask,

diff --git a/introduction.tex b/introduction.tex
index 654cb1f..36ef589 100644 (file)
--- a/introduction.tex
+++ b/introduction.tex
@@ -114,8 +114,13 @@ Again, this requires a reprogramming cycle every time the
 Another \gls{EDSL} designed to generate low-level high-assurance programs is
 called \gls{Ivory} and uses \gls{Haskell} as a host language%
 \cite{elliott_guilt_2015}. The language uses the \gls{Haskell} type-system to
-make unsafe language type safe. \gls{Ivory} has been used in for example the
+make unsafe languages type safe. \gls{Ivory} has been used in for example the
 automotive industry to program parts of an autopilot%
-\cite{pike_programming_2014}\cite{hickey_building_2014}. A dialect of the
-\gls{Ivory} called \gls{Tower} has also been created by the same authors which
-is has specific backends for \glspl{RTOS}.
+\cite{pike_programming_2014}\cite{hickey_building_2014}. \Gls{Ivory}'s syntax
+is deeply embedded but the type system is shallowly embedded. This requires
+several \gls{Haskell} extensions that offer dependant type constructions. The
+process of compiling an \gls{Ivory} program happens in stages. The embedded
+code is transformed into an \gls{AST} that is sent to a backend. The
+\gls{mTask} \gls{EDSL} transform the embedded code during compile-time directly
+into the backend which is often a state transformer that will execute on
+runtime.\todo{Misschien een beetje onduidelijk of kort?}