diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 536d58d04a9c5ce2bf80872c68b42aecf5c0aa43..1f2aa1d8c70b1c7c8ac694c145a2268c8c79f9c1 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -449,7 +449,9 @@ multiple options and to address high scientific and technological
 risks.
 } 
 
-\oldt{Our proposed \azx language is an advanced \textsc{zx}-style system
+\benREM{I think this part is more or less OK to keep ``as it''.}
+
+Our proposed \azx language is an advanced \textsc{zx}-style system
 augmented with features needed for applications.  The \zxcalculus
 occupies a place in quantum computation similar to the
 $\lambda$-calculus in classical computing: it provides a solid but
@@ -479,7 +481,7 @@ Development of such techniques is a low-risk extension of earlier
 work, and will be done early in the project
 (\ref{task:algorithms},\ref{task:basic-opt}). Further, at this stage
 a program can be translated to a fault-tolerant equivalent with
-respect to a chosen error-correcting code.}
+respect to a chosen error-correcting code.
 
 % \REM{Can do useful stuff at this level!  Some optimisation; ECC
 % simple generic optimisations.  e.g.
@@ -497,8 +499,7 @@ respect to a chosen error-correcting code.}
 
 
 
-
-\oldt{The annotations of the second layer provide the basis of \emph{augmented
+The annotations of the second layer provide the basis of \emph{augmented
   rewrites}: program transformations which are guided by the
 annotations to achieve particular goals, not expressible in the basic
 tensor language.  For instance, there is an efficient algorithm
@@ -552,7 +553,7 @@ project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
 Early in the project, we will implement translations from existing
 quantum programming languages~(\ref{task:trans1}).  These will provide
  examples and test cases, and allow comparative
-evaluation.} % of the \azx system.  %We will adapt an existing compiler to generate parameterised \azx terms (\ref{task:trans2}).
+evaluation. % of the \azx system.  %We will adapt an existing compiler to generate parameterised \azx terms (\ref{task:trans2}).
 
 % Due to the fact that there exist ZX-based software, additional features were added to the language e.g.~`bang-boxes' which are formal incarnations of the ``..." occurring in the above equations. 
 
@@ -563,7 +564,6 @@ evaluation.} % of the \azx system.  %We will adapt an existing compiler to gener
 
 % \REM{Risk assessment: which are easy, which are hard?  Dependencies.}
 
-\REM{WHY this is a good idea.}
 
 
 
@@ -614,7 +614,7 @@ various themes: the relation between \zx and other quantum computing representat
 \subsubsection{A quantum compiler stack}
 \label{sec:progr-lang-supp}
 
-\oldt{In the quantum setting, several powerful high-level languages
+In the quantum setting, several powerful high-level languages
 (HLLs) such as Quipper~\cite{Alexander-S.-Green:2013fk} and Q\#
 \cite{qsharp} have been proposed.  As in the case of their
 classical counterparts, these HLLs are not designed to be run directly
@@ -630,24 +630,15 @@ general framework for compilation of HLLs to \azx.
 
 Since most existing quantum HLLs can output circuit descriptions, and
 since circuits can easily be represented in the \zxcalculus, we first
-design a simple front end for the circuit language
-QASM~\cite{Cross2017Open-Quantum-As} in 
-\ref{task:transQASM}.  This will allow \azx terms to be produced from
-virtually any extant quantum HLL, albeit rather naively.
-Later, we will perform concrete front-end experiments using more
-sophisticated existing HLLs, for example \emph{Quipper},
-Q\#~\cite{qsharp}, or ProjectQ \cite{Steiger2016ProjectQ:-An-Op} during the
-long running task~\ref{task:transHLL}.  
-
-This work package consists of a back-and-forth interaction between
-HLLs and \azx, which is why many of its tasks span the entire lifetime
-of the project. HLL development influences \azx by providing the
-control structures and other constructs that must be represented at
-\azx level. Conversely, \azx developments will influence HLL, as we
-analyse how information and requirements from the back-end flow upward
-in a meaningful way, and how this can be translated into compilation
-flags and assertions/hints to the compiler within HLL programs. 
-
+focus on a simple front end for the circuit language
+QASM~\cite{Cross2017Open-Quantum-As} in \ref{task:testBench}.  This
+will allow \azx terms to be produced from virtually any extant quantum
+HLL, albeit rather naively.  Later, we will perform concrete front-end
+experiments using more sophisticated existing HLLs, for example
+\emph{Quipper}, Q\#~\cite{qsharp}, or ProjectQ
+\cite{Steiger2016ProjectQ:-An-Op} during the
+task~\ref{task:betterboxes}.
+%
 The open database of tests developed in \ref{task:testBench} will
 serve as a measuring tool for the quality of the output. The database
 will also be made available to the community for rating and testing
@@ -656,6 +647,16 @@ from other research groups, and to support other languages, both our
 interface and the \azx language will be made
 public.
 
+%% OUTDATED
+% This work package consists of a back-and-forth interaction between
+% HLLs and \azx, which is why many of its tasks span the entire lifetime
+% of the project. HLL development influences \azx by providing the
+% control structures and other constructs that must be represented at
+% \azx level. Conversely, \azx developments will influence HLL, as we
+% analyse how information and requirements from the back-end flow upward
+% in a meaningful way, and how this can be translated into compilation
+% flags and assertions/hints to the compiler within HLL programs. 
+
 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
@@ -666,9 +667,40 @@ 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} In a hybrid architecture like NQIT, these
-properties will vary across the subsystems, with concomitant
-implications for the execution of the desired program.
+modes.\REM{noise,fidelitY}
+
+Due to its novelty, we adopt an exploratory approach.  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.  We will use these examples to develop
+prototypical \azx constructs expressing the relevant properties.  This
+consists in three tightly related tasks: decomposing the tensor
+network into atomic operations; characterising runnability with
+respect to the model by predicates in monadic second order logic; and
+transforming the tensor network into an equivalent runnable version.
+This experience will inform the later work in \ref{wp:theory} and
+\ref{wp:usefulstuff}.
+
+Although we will provide specific modules for the tasks described above, the
+\azx system is intended to extensible, so we will also publish an open
+API and specification language to simplify the task of adding new
+architectures and error correcting schemes to the system
+(\ref{task:backendapi}). 
+
+
+%% OUTDATED
+%In a hybrid architecture like NQIT, these
+%properties will vary across the subsystems, with concomitant
+%implications for the execution of the desired program.
+
+
+
+
+\subsubsection{Representation, reasoning, and resources}
+\label{sec:machines-models}
+
+\REM{stuff about WP 2 here}
 
 Since the overall goal of the project is to produce a
 \emph{retargetable} compiler, able to generate executables for
@@ -682,17 +714,11 @@ characteristics and architectural constraints of various idealised and
 realistic machines, and develop language features of \azx to express
 these properties.  The goal is two-fold: to facilitate
 \emph{code-generation} for a given machine from an \azx term; and to
-expose information needed by the \emph{optimiser}.}
+expose information needed by the \emph{optimiser}.
 
 
-
-\subsubsection{Representation, reasoning, and resources}
-\label{sec:machines-models}
-
-\REM{stuff about WP 2 here}
-
 \oldt{
-A key research challenge of this work package consists in the
+  A key research challenge of this work package consists in the
 management of the {\em classical computation} and {\em classical
   information} within quantum algorithms: What computation should
 occur at the \azx-generation phase, and which classical parameters are
@@ -701,19 +727,6 @@ design a test suite (\ref{task:testBench}) to compare possible
 solutions.
 
 
-Due to its novelty, we adopt an exploratory approach.  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.  We will use these examples to develop
-prototypical \azx constructs expressing the relevant properties.  This
-consists in three tightly related tasks: decomposing the tensor
-network into atomic operations; characterising runnability with
-respect to the model by predicates in monadic second order logic; and
-transforming the tensor network into an equivalent runnable version.
-This experience will inform the later work in \ref{wp:theory} and
-\ref{wp:usefulstuff}.
-
 While in the early stages of the project, it will already be quite
 useful to study concrete diagrams of fixed size (e.g. a quantum
 circuit on $N$ qubits for a previously-fixed $N$), in task
@@ -832,11 +845,6 @@ or after layout, depending on the circumstances.  Layout will be handled
 in a similar way to this second kind of optimisation, generalising
 from \ref{task:delft-model} and \ref{task:NQIT-model}.
 
-Although we will provide specific modules for the tasks described above, the
-\azx system is intended to extensible, so we will also publish an open
-API and specification language to simplify the task of adding new
-architectures and error correcting schemes to the system
-(\ref{task:backendapi}). 
 
 The tasks to be performed within WP4 may be broadly described in terms of how the \azx compiler will transform \zx terms produced by the front-end to obtain instructions to be realised by a quantum computer (or software quantum simulator) at the back-end.
 These stages are: (i)~an initial round of generic, hardware-independent optimisations; (ii)~application of some choice of strategy for error correction; (iii)~translation to a specialised annotation system which represents the parameters and constraints of a specific hardware implementation; and finally (iv)~another round of optimisation within the constraints imposed by the error correction and hardware models.
@@ -2413,3 +2421,8 @@ with very large graphs.
 }
 
 \end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/NEWPROPOSAL/preamble.tex b/NEWPROPOSAL/preamble.tex
index d39ff503a5acddaa15914ff9b6bd2f8a95e5aae7..3136e491787b37e6440a6804b72c0e1edafe5344 100644
--- a/NEWPROPOSAL/preamble.tex
+++ b/NEWPROPOSAL/preamble.tex
@@ -274,8 +274,10 @@
 
 \newcommand{\zx}{\textsc{zx}\xspace}
 \newcommand{\zxcalculus}{\textsc{zx}-calculus\xspace}
-\newcommand{\azx}{\texttt{\bfseries\color{red!70!black} [REDEFINE \textbackslash azx MACRO]}\xspace}
-\newcommand{\liquid}{\texttt{\bfseries\color{red!70!black} [CONSIDER REPLACING REFERENCE TO LIQUID BY Q\#]}\xspace}
+\newcommand{\azx}{\texttt{\bfseries\color{red!70!black}AZX}\xspace}
+\newcommand{\liquid}{\texttt{\bfseries\color{red!70!black}Q\#}\xspace}
+
+\newcommand{\benREM}[1]{\texttt{\bfseries\color{red!70!black} [{#1}]}\xspace}
 
 \usepackage{pgfgantt}