X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FFuture.tex;h=9c60dfe8e3b8f656ef0bd8a74e67fa6a98b4e80b;hp=daeee3fd10844b351fde9109a96656bd73bd79b5;hb=b2047c9f1622d62aecc6708dd19c38b14810f275;hpb=100a8917713c1300a2002299cea94b04ac66848a

diff --git a/Chapters/Future.tex b/Chapters/Future.tex
index daeee3f..9c60dfe 100644
--- a/Chapters/Future.tex
+++ b/Chapters/Future.tex
@@ -391,8 +391,8 @@ behaviour is not needed.
 
 The main cost of this approach will probably be extra complexity in the
 compiler: The paths (state) data can take become very non-trivial, and it
-is probably hard to properly analyze these paths and produce the intended VHDL
-description.
+is probably hard to properly analyze these paths and produce the
+intended \VHDL description.
 
 \section{Multiple cycle descriptions}
 In the current Cλash prototype, every description is a single-cycle
@@ -616,4 +616,12 @@ lightly.
   methods for describing don't care conditions. Possibly there are completely
   other methods which work better.
 
+\section{Correctness proofs of the normalization system}
+As stated in \in{section}[sec:normalization:properties], there are a
+number of properties we would like to see verified about the
+normalization system.  In particular, the \emph{termination} and
+\emph{completeness} of the system would be a good candidate for future
+research. Specifying formal semantics for the Core language in
+order to verify the \emph{soundness} of the system would be an even more
+challenging task.
 % vim: set sw=2 sts=2 expandtab: