-\section{\acrlong{EDSL}s}
-There are several techniques available for creating \glspl{EDSL}. Each of
-them have their own advantages and disadvantages such as extendability,
-typedness and view support. In the following subsections each of the main
-techniques are briefly explained.
-
-\subsection{Deep embedding}
-A deep \gls{EDSL} means that the language is represented as an \gls{ADT}. Views
-are functions that transform something to the datatype or the other way around.
-As an example we have the simple arithmetic \gls{EDSL} shown in
+An \gls{EDSL} is a language embedded in a host language. \glspl{EDSL} can have
+one or more backends or views. Commonly used views are pretty printing,
+compiling, simulating, verifying and proving the program. There are several
+techniques available for creating \glspl{EDSL}. Each of them have their own
+advantages and disadvantages in terms of extendability, typedness and view
+support. In the following subsections each of the main techniques are briefly
+explained.
+
+\section{Deep embedding}
+A deep \gls{EDSL} is a language represented as an \gls{ADT}. Views are
+functions that transform something to the datatype or the other way around. As
+an example we have the simple arithmetic \gls{EDSL} shown in