diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index c350ddbde9b8e1c00627c1c0d2b1ef99c4635172..7ba6412ffdf64e9b98042adfe8b2e83280c564ac 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -254,7 +254,19 @@ An example of such a transformation is the following:}
     %\cnotv[0.6] \rTo^* 
     \cnotvi[0.7]
   \]~\\[-4mm]%
-Members of our consortium have demonstrated how to use these formal reasoning techniques in software, including the interactive theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which was used to formally verify quantum communication protocols and error correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr}) and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early demonstration of the capacity of the \zxcalculus to \newt{outperform other methods of circuit optimisation,  in the sense that certain circuit metric (such as total size, tree-width, or number of non-Clifford subterms such as T-gates) can be minimised.}
+Members of our consortium have demonstrated how to use these formal
+reasoning techniques in software, including the interactive theorem
+prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which
+was used to formally verify quantum communication protocols and error
+correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr})
+and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early
+demonstration of the capacity of the \zxcalculus to \newt{outperform
+  other methods of circuit optimisation,  in the sense that certain
+  circuit metric (such as total size, tree-width, or number of
+  non-Clifford subterms such as T-gates) can be minimised.}  Our
+industry partner CQC develops \tket, a retargetable quantum compiler
+which, using \zx-based optimisations, outperforms all existing
+compilers for quantum software.
 \TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
 %%% cutting because repeated later
 % It is strictly more powerful than the stabiliser
@@ -489,10 +501,10 @@ equivalent, space-optimal circuit \cite{Duncan:2010aa}.
 The \dzxc system
 would generalise this concept to encompass other sorts of information which would inform how to transform (i.e.,~to re-write) a generic representation of a quantum computational procedure.
 For example, 
-the \dzxc system could encorporate
+the \dzxc system could incorporate
 a system which specifies both how to represent logical operations in a particular error correcting code, and how the operations are constrained in order to satisfy basic precautions to keep the realisation fault-tolerant (\ref{task:ECC}).
 This would enable the \dzxc system
-to re-write procedures, to minimise the number of operations subject to the constraints described by those annotations.
+to re-write procedures, minimising the number of operations, subject to the constraints described by those annotations.
 
 The \dzxc system will be modular, and allow for several different systems of annotations, for different hardware platforms or constraints one might impose on a computation.
   One such system of annotations would be to describe
@@ -582,14 +594,14 @@ idea of separating program compile time from circuit compile time
 }
 
 The four major work packages of the project are structured into
-various themes: the relation between \zx and other quantum computing representations (\ref{wp:frontend});  necessary theoretical developments of \zx (\ref{wp:backends}); optimisation strategies independent of implementations (\ref{wp:theory}); using enriched \zx to compile and optimise for specific quantum devices.(\ref{wp:usefulstuff}).
+various themes: the relation between \zx and other quantum computing representations (\ref{wp:frontend});  necessary theoretical developments of \zx (\ref{wp:backends}); optimisation strategies independent of implementations (\ref{wp:theory}); using annotated \zx to compile and optimise for specific quantum devices.(\ref{wp:usefulstuff}).
 
 \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},
-  \Qsharp~\cite{qsharp}, and the Python library
+  \Qsharp~\cite{qsharp}, and the Python framework
   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.
@@ -611,18 +623,18 @@ various themes: the relation between \zx and other quantum computing representat
 
 %
   Moving down the compilation toolchain towards quantum devices
-  requires the traduction of \zx terms down to some lower-level
+  requires the translation 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.
-Realistic models of such devices integrates various restrictions such
+Realistic models of such devices include 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, be subject to various noise model and suffer from low fidelity.
+modes, be subject to various noise models, and suffer from low fidelity.
 \REM{noise,fidelitY}
 %
 Due to the novelty of our proposal, we adopt an exploratory approach
@@ -650,8 +662,9 @@ This experience will inform the later work in \ref{wp:theory} and
 To encourage interaction from other research groups, and to support other languages, the interfaces and functionality for the \dzxc system will be made public.
 While we will provide specific modules for the tasks described above, the \dzxc system is intended to extensible: therefore we will 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 database will be made available to the community for rating and testing future compilers or optimisation techniques.
-Furthermore, in Task~\ref{task:testBench}, we will develop an open database of tests, which will serve as a measuring tool for the quality of the output from the \dzxc compiler.
+Furthermore, in Task~\ref{task:testBench}, we will develop an open
+database of tests, which will serve as a measuring tool for the
+quality of the output from the \dzxc compiler.  The database will be made available to the community for rating and testing future compilers or optimisation techniques.
 
 \subsubsection{Representation, reasoning, and resources}
 \label{sec:machines-models}
@@ -693,12 +706,13 @@ With this we will further develop the usefulness of \zx as a way in which to des
 This may provide insight on outstanding open problems beyond the scope of the current proposal. 
 
 The question of resources for quantum speedup will be the topic of Task \ref{task:resources}.
-Different paradigms of computation, such as Clifford, Clifford+T, and universal qubit QM, have been recently axiomatised from the scope of \zx.
+Different paradigms of computation, such as Clifford, Clifford+T, and
+universal qubit QM, have been recently axiomatised in the language of \zx.
 Each of those paradigms, however, offer different degrees of computational power.
 By a comparative study of such axiomatic representations, we will aim at identifying, in the \zx language, what is the feature that enables quantum speed-up.
 That is, we will characterise quantum resources in a systematic manner using the \zx framework.
 By further building a bridge from the \zx formulation and traditional (e.g.,~device independent) approaches to quantum resources, we will be able to contrast our findings with the current intuitions of what may power quantum computing.
-These current intuitions include the nonclassical feature of Nature called Kochen--Specker contextuality, as well as Bell nonlocality.
+These current intuitions include the nonclassical feature of nature called Kochen--Specker contextuality, as well as Bell nonlocality.
 Hence, the outcome of \ref{task:resources} will also include the development of \newt{representations} %proofs 
 of contextuality within the \zx language.
 
@@ -726,7 +740,7 @@ The formal mechanism which the \dzxc system will use to transform \zx terms (sou
 are the theoretical core of this proposal.
 Developing effective techniques for mapping \zx terms closely to the constraints of hardware is a prerequisite for our success.
 
-We forsee three stages in the compilation process of a \zx
+We forsee four stages in the compilation process of a \zx
 term into instructions for a physical machine.
 %The tasks to be performed within \ref{wp:theory} and \ref{wp:usefulstuff} may be broadly described in terms of how the \dzxc system 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:
@@ -808,7 +822,7 @@ We identify three main tasks:
 Although we treat them separately, in practice these tasks
 will interact in non-trivial ways, and their order need not be fixed.
 
-The annotation system for hardware constraints the abstract rewrite theory of \zx-diagrams and real-world constraints coming from quantum hardware.
+The annotation system overlays the abstract rewrite theory of \zx-diagrams with real-world constraints coming from quantum hardware.
 We will then develop the formal tools for rewriting \zx-diagrams in ways that
 respect those constraints. 
 In task \ref{task:annotate2} we will explore methods to annotate a \zx-diagram with quantitative information such as timing, noise, or fidelity.