From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 24 May 2017 13:28:12 +0000 (+0200)
Subject: update stukje over ivory
X-Git-Tag: hand-in~114
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=faca758c348718411803e4b8fab3a83a85665d1a;p=msc-thesis1617.git

update stukje over ivory
---

diff --git a/acronyms.tex b/acronyms.tex
index 2481539..ac1d001 100644
--- 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
--- 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
--- 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?}