Continue intro a little

report/report.tex

@@ -39,6 +39,39 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Introduction}
 
+In the previous years, verification and proved software has gathered an
+increasing interest in the computer science community, as people realised how
+hard bugs are to track down. But hardware bugs are even more tedious to find
+and fix, and can easily lead to disastrous consequences, as those cannot be
+patched on existing hardware. For instance, the well-known Pentium
+``\textsc{fdiv}'' bug~\ref{pratt1995fdiv} that affected a large number of
+Pentium processors lead to wrong results for some floating point divisions.
+Intel had to replace \todo{how many?} CPUs, leading to a loss of \todo{how
+much?}. Even recently, the Skylake and Kiby Lake \todo{(?)} hyperthreading bug
+had to be patched using microcode, loosing performance and reliability.
+
+To avoid such disasters, the industry nowadays uses a wide range of techniques
+to catch bugs as early as possible -- which, hopefully, is before the product's
+release date. Among those are \todo{list + cite}, but also proved hardware. On
+circuits as complex as processors, usually, only sub-components are proved
+correct in a specified context -- that should, but is not proved to, be
+respected by the other parts of the circuit. Yet, this trade-off between proved
+correctness and engineer's work time already gives a pretty good confidence in
+the circuit.
+
+In this context, Carl Seger was one of the \todo{the?} main developer of FL
+\todo{(?, acronym?)} at Intel, a functional programming language integrating
+many features useful to get insights of a circuit, testing it and proving it.
+Among other features, it includes a ``search and replace'' feature, which can
+search every occurrence of a given gates pattern in a circuit, and replace it
+by some other gates pattern, proved observationally equivalent.\\
+Time has proved this method very efficient to design circuits: this way, one
+can start from an inefficient, yet simple circuit, prove it, and then refine it
+into an equivalent, yet efficient one, through proved transformations. It is
+also possible to go the other way, and start with an optimized circuit, hard to
+understand, and make it easier to understand to work more efficiently.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Context \& AST}
 
 \todo{Rename this section}\\