more rewording

practical.tex

-We have implemented the algorithmic system $\vdashA$. Our implementation is written in OCaml and uses CDuce as a library to
+We have implemented the algorithmic system $\vdashA$. Our
+implementation is written in OCaml and uses CDuce as a library to
 provide the semantic subtyping machinery. Besides a type-checking
 algorithm defined on the base language, our implementation supports
-record types (Section \ref{ssec:struct}) and the refinement of function types
-(Section \ref{sec:refining} with the rule of Appendix~\ref{app:optimize}). The implementation is rather crude and
+record types (Section \ref{ssec:struct}) and the refinement of
+function types (Section \ref{sec:refining} with the rule of
+Appendix~\ref{app:optimize}). The implementation is rather crude and
 consists of 2000 lines of OCaml code, including parsing, type-checking
-of programs, and pretty printing of types. We demonstrate the output of
-our type-checking implementation in Table~\ref{tab:implem}. These
-examples and others can be tested in the online toplevel available at
+of programs, and pretty printing of types. We demonstrate the output
+of our type-checking implementation in Table~\ref{tab:implem} by
+listing some examples none of which can be typed by current
+systems (even though some system such as Flow and TypeScript
+can type some of them by adding explicit type annotation, the code 6,
+7, 9, and 10 and the \code{and\_} and \code{xor\_} functions at the end of this
+section are out of reach of current systems, even when using the right
+explicit annotations). These examples and others can be tested in the
+online toplevel available at
 \url{https://occtyping.github.io/}%
 \ifsubmission
 ~(the corresponding repository is