Remarks in documentation

src/sphinx/intro.rst

@@ -13,16 +13,46 @@ unique automation functionality. In particular, Leon can
 * automatically execute and synthesize working functions
   from partial input/output specifications and test cases.
 
+Leon and Scala
+--------------
+
+Leon attempts to strike a delicate balance between the convenience 
+of use on the one hand and the simplicity of reasoning 
+on the other hand. 
 Leon primarily supports programs written in :ref:`Pure Scala <purescala>`, a purely
-functional subset of Scala.  That said, the :ref:`XLang <xlang>` extension enables Leon to
-work on a richer subset of Scala, including imperative features. 
-The :ref:`Pure Scala <purescala>` features are at the *core* of the Leon
+functional subset of Scala. 
+This fragment is at the core of 
+the functional programming paradigm and lies at the intersection
+of functional languages such as Scala, Haskell, ML, and fragments present in interactive theorem provers such as Isabelle and Coq. Thus,
+if you do not already know Scala, learning the Leon subset should
+be easier as it is a smaller language.
+The :ref:`Pure Scala <purescala>` features are at the core of the Leon
 system. They are considered as primitives and get a personalized treatment in
-the solving algorithms of Leon. On the other hand, features introduced by
-:ref:`XLang <xlang>` are handled by translation into Pure Scala
-concepts. They are often more than just syntactic sugar, because some of them
-require significant modification of the original program, such as introducing
-additional parameters to a set of functions.
+the solving algorithms of Leon. 
+Leon's algorithms can map this fragment into the first-order language
+of SMT (satisfiability modulo theory) solvers, enabling
+efficient automated reasoning. Moreover, thanks to the use of 
+``scalac`` front end, Leon supports implicits and ``for`` 
+comprehensions (which also serve as a syntax for monads in Scala).
+Leon also comes with a simple library of useful data types, which are designed
+to work well with automated reasoning and Leon's language fragment.
+
+In addition to this pure fragment, Leon supports the
+:ref:`XLang <xlang>` extension, which enables Leon to work
+on a richer subset of Scala, including imperative features.
+Features introduced by :ref:`XLang <xlang>` are handled by
+translation into Pure Scala concepts. They are often more
+than just syntactic sugar, because some of them require
+significant modification of the original program, such as
+introducing additional parameters to a set of functions.  As
+an intended aspect of its current design, Leon's language
+currently does not provide a default encoding of
+e.g. concurrency with a shared mutable heap, though it might
+support more manageable forms of concurrency in the future.
+For practical reasons, Leon programs can also call out into
+general Scala code, which needs to be used with care as it
+is a form of "foreign function interface" into the general
+world of Scala.
 
 If you would like to use Leon now, check the :ref:`Getting Started <gettingstarted>`
 section and try our :ref:`Tutorial <tutorial>`.

src/sphinx/library.rst

@@ -3,15 +3,33 @@
 Leon Library
 ============
 
-Leon defines its own versions of most data structures. One
-of the reasons is to ensure that these operations can be
-correctly mapped to mathematical functions and relations
-inside of SMT solvers, largely defined by the SMT-LIB
-standard (see http://www.smt-lib.org/).
+Leon defines its own library with some core data types and
+operations on them, which work with the fragment supported
+by Leon. One of the reasons for a separate library is to
+ensure that these operations can be correctly mapped to
+mathematical functions and relations inside of SMT solvers,
+largely defined by the SMT-LIB standard (see
+http://www.smt-lib.org/). Thus for some data types, such as
+``BigInt``, Leon provides a dedicated mapping to support reasoning.
+(If you are a fan
+of growing the language only through libraries, keep in mind that 
+growing operations together with the ability to reason about them
+is what the development of mathematical theories is all about, and
+is a process slower than putting together 
+libraries of unverified code--efficient automation of reasoning about a 
+single decidable theory generally results in multiple research papers.)
+For other operations (e.g., `List[T]`), the library
+is much like Leon user-defined code, but specifies some
+useful preconditions and postconditions of the operations, thus
+providing reasoning abilities using mechanisms entirely available
+to the user.
 
 To use Leon's libraries, you need to use the appropriate
 `import` directive at the top of Leon's compilation units.
-Here is a quick summary of what to import.
+Here is a quick summary of what to import. 
+For the most up-to-date version of the library,
+please consult the ``library/`` directory in your Leon
+distribution.
 
 +--------------------------------+----------------------------------------------------+
 | Package to import              | What it gives access to                            |