diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 6d4c0d40ea4dfdce203c469096f36649717b9843..d6361e8eb684efae6eea36d6a06caec93a1d6c43 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -589,7 +589,10 @@ various themes: the relation between \zx and other quantum computing representat
 \subsubsection{A quantum compiler stack}
 \label{sec:progr-lang-supp}
 
-  Several powerful high-level languages (HLLs) have been proposed for quantum programs, such as Quipper~\cite{Alexander-S.-Green:2013fk} and \Qsharp~\cite{qsharp}.
+  Several powerful high-level languages (HLLs) have been proposed for
+  quantum programs, such as Quipper~\cite{Alexander-S.-Green:2013fk},
+  \Qsharp~\cite{qsharp}, and the Python library
+  ProjectQ~\cite{Steiger2016ProjectQ:-An-Op}.
   As with classical HLLs, these languages are not designed to be run directly on quantum hardware: instead, their compilers typically output quantum circuit descriptions, which are not tailored well to run on any particular hardware platform.
   Our proposed \dzxc system will represent an interface between multiple different HLLs for quantum procedures, and various quantum hardware platforms.
   This system will use terms of the \zxcalculus as an internal representation of the procedure as it undergoes optimisations and translations, \newt{both abstractly and} to fit a particular hardware architecture.
@@ -597,30 +600,44 @@ various themes: the relation between \zx and other quantum computing representat
   but would be generated by a compiler front-end from programs written in existing high-level languages.
   Therefore it is essential to provide a robust, general framework for compilation of HLLs to \zx terms.
 
-  As most existing quantum HLLs can output circuit descriptions, and as circuits can easily be represented in the \zxcalculus, \newt{in \ref{task:HHL}} we first focus on a simple front end for the circuit language QASM~\cite{Cross2017Open-Quantum-As} before moving towards more expressive HHLs.
-  This will allow virtually any extant quantum HLL to interface with the \dzxc system, albeit rather naively at first.
-Later, we will perform concrete front-end
-experiments using more sophisticated existing HLLs in, for example
-\emph{Quipper}, \Qsharp~\cite{qsharp}, or ProjectQ
-\cite{Steiger2016ProjectQ:-An-Op}, with the help of \newt{Task~\ref{task:trans1}}.
+  As most existing quantum HLLs can output circuit descriptions, and
+  as circuits can easily be represented in the \zxcalculus, for the
+  front-end of~\ref{task:HHL} will first focus on the circuit language
+  QASM~\cite{Cross2017Open-Quantum-As} before moving towards the more
+  expressive HHLs Quipper~\cite{Alexander-S.-Green:2013fk},
+  \Qsharp~\cite{qsharp}, and
+  ProjectQ~\cite{Steiger2016ProjectQ:-An-Op}. With this expertise we
+  will then develop in Task~\ref{task:trans1} a general procedure
+  allowing virtually any extant quantum HLL to interface with the
+  \dzxc system.
 
+%
+  Moving down the compilation toolchain towards quantum devices
+  requires the traduction of \zx terms down to some lower-level
+  representation, specific to each quantum device.
+%
 Proposed and existing quantum devices differ along a variety of axes.
-At the most abstract level, the quantum circuit model and the
-1-way model \cite{Raussendorf-2001} have different execution
-concepts and primitive operations, despite their computational
-equivalence.  More realistic models might suffer from limitation to a
+Realistic models of such devices integrates various restrictions such
+as the  limitation to a
 fixed number of qubits, a bounded total execution time, or
 restrictions on which qubits may interact directly.  
 %Looking more closely, 
 Primitive operations will require different amounts of time,
 different qubit implementations have different failure
-modes.\REM{noise,fidelitY}
+modes, be subject to various noise model and suffer from low fidelity.
+\REM{noise,fidelitY}
 %
-Due to the novelty of our proposal, we adopt an exploratory approach with respect to back-end models.
-Initially, and in parallel, we study the circuit model (\ref{task:circuit-model}) and
-the 1-way model (\ref{task:mbqc-model}) because these models are well understood, stable, and have been extensively treated in the \zxcalculus literature. 
-  These models will allow us to prototype the development of hardware annotations for the \dzxc system, \newt{cf.\ Task~\ref{task:runnable}}.
-  In both cases, this involves three tightly related tasks:
+Due to the novelty of our proposal, we adopt an exploratory approach
+with respect to back-end models.  Initially, and in parallel, we study
+the circuit model (\ref{task:circuit-model}) and the 1-way
+model~\cite{Raussendorf-2001} (\ref{task:mbqc-model}). On one hand,
+these models are well understood, stable, and have been extensively
+treated in the \zxcalculus literature.  On the other hand, these two
+models have different execution concepts and primitive operations,
+despite their computational equivalence. They will therefore allow us
+to prototype the development of hardware annotations for the \dzxc
+system, \newt{cf.\ Task~\ref{task:runnable}}.  In both cases, this
+involves three tightly related tasks:
   \begin{enumerate}[label=(\roman*)]
   \item
     decomposing the tensor network into atomic operations;