Fix abstract

2 files changed, 10 insertions, 3 deletions

diff --git a/draft.org b/draft.org
index 92ffecd..35ded64 100644
--- a/draft.org
+++ b/draft.org
@@ -27,3 +27,11 @@
 
 - ramp up more about the future.
 - formally verifying other algorithms
+
+TODO:
+- move second part of first paragraph.
+- add to intro what this document is
+- last paragraph more like last part of abstract (To that end we have made one.)
+- Separate second point into are already reliable and existing testing techniques are enough.
+- Most hardware designs start in C.
+- First John bacceses fortran compiler.
diff --git a/main.tex b/main.tex
index 9e9864b..6b478a1 100644
--- a/main.tex
+++ b/main.tex
@@ -145,10 +145,9 @@
 % - But there's still a long way to go. (List the main things left to do, and how you expect Vericert to compare to LegUp after those things are done.)
 
 \begin{abstract}
-  High-level synthesis (HLS) is increasingly being relied upon as the size of designs and needs for hardware accelerators increases.
-  \JW{I'd be tempted to switch that around to make a more interesting opening: `With hardware designs becoming ever more complex and demand for custom accelerators ever growing, high-level synthesis (HLS) is increasingly being relied upon.'} However, HLS is known to be quite flaky \JW{,} with each tool supporting \JW{subtly} different \JWreplace{input languages}{fragments of the input language} and sometimes even generating incorrect designs.
+  With hardware designs becoming ever more complex and demand for custom accelerators ever growing, high-level synthesis (HLS) is increasingly being relied upon.  However, HLS is known to be quite flaky, with each tool supporting subtly different fragments of the input language and sometimes even generating incorrect designs.
 
-  We argue that \JWreplace{formally verifying HLS}{a formally verified HLS tool} could solve this issue by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. \JWcouldcut{In this respect,} \JW{To this end,} we have developed \vericert{}, a formally verified HLS tool, based on \compcert{}, a formally verified C compiler.
+  We argue that a formally verified HLS tool could solve this issue by dramatically reducing the amount of trusted code, and providing a formal description of the input language that is supported. To this end, we have developed \vericert{}, a formally verified HLS tool, based on \compcert{}, a formally verified C compiler.
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts