Merge pull request #36 from coq/rework-recommended-books

Update recommended books for beginner and intermediate levels.

data/books/mathcomp.md

@@ -2,13 +2,11 @@
 title: "Mathematical Components"
 slug: "mathcomp"
 description: >
-  Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra.
+  Mathematical Components is the name of a library of formalized mathematics for the Rocq Prover. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra.
 recommendation: >
-  Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order Theorem.
-  This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Coq system and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology proposed in other sources. As a consequence, this book provides a slightly non-standard presentation of Coq, putting upfront the formalization choices and the proof style that are the pillars of the library.
-  This books targets two natures of audience. On one hand newcomers, in particular beginners with background in mathematics rather than computer science, should find a soft introduction to the programming language of Coq, Gallina, and to the Ssreflect proof language. On the other hand, accustomed Coq users will find a substantial account of the formalization style that made the Mathematical Components library possible.
+  For newcomers with a background in mathematics rather than computer science, this book is an introduction to the Rocq Prover and to the SSReflect proof language used in the Mathematical Components library. Accustomed Rocq users will find a substantial account of the formalization style that made the Mathematical Components library possible.
 authors:
-  - Assia Mahboubi 
+  - Assia Mahboubi
   - Enrico Tassi
 published: 2022/09/28
 cover: books/mathcomp.png
@@ -23,9 +21,8 @@ pricing: free
 
 
 
-Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order Theorem.
+Mathematical Components is the name of a library of formalized mathematics for the Rocq Prover. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order Theorem.
 
-This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Coq system and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology proposed in other sources. As a consequence, this book provides a slightly non-standard presentation of Coq, putting upfront the formalization choices and the proof style that are the pillars of the library.
-
-This books targets two natures of audience. On one hand newcomers, in particular beginners with background in mathematics rather than computer science, should find a soft introduction to the programming language of Coq, Gallina, and to the Ssreflect proof language. On the other hand, accustomed Coq users will find a substantial account of the formalization style that made the Mathematical Components library possible.
+This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Rocq Prover and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology proposed in other sources. As a consequence, this book provides a slightly non-standard presentation of Rocq, putting upfront the formalization choices and the proof style that are the pillars of the library.
 
+This books targets two natures of audience. On the one hand newcomers, in particular beginners with background in mathematics rather than computer science, should find a soft introduction to the programming language of the Rocq Prover, Gallina, and to the SSReflect proof language used in the Mathematical Components library. On the other hand, accustomed Rocq users will find a substantial account of the formalization style that made the Mathematical Components library possible.

data/books/software-foundations-1.md

@@ -3,9 +3,9 @@ title: "Software Foundations: Logical Foundations (Volume 1)"
 slug: "software-foundations-1"
 description: >
   The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.
+  Logical Foundations is the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving, and the Rocq Prover.
 recommendation: >
-  Logical Foundations is the entry-point to the series. It covers functional programming, basic concepts of logic, 
-  computer-assisted theorem proving, and Rocq.
+  For newcomers interested in programming languages, the Software Foundations series is an excellent introduction to using the Rocq Prover for formal verification.
 authors:
   - Benjamin C. Pierce
   - and many others
@@ -24,5 +24,4 @@ pricing: free
 
 The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Rocq Prover.
 
-Logical Foundations is the entry-point to the series. It covers functional programming, basic concepts of logic, 
-  computer-assisted theorem proving, and Rocq.
+Logical Foundations is the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving, and the Rocq Prover.

src/rocqproverorg_frontend/pages/learn.eml

@@ -84,10 +84,16 @@ Learn_layout.single_column_layout
 
     <div class="grid gap-6 mt-6 lg:grid-cols-2">
       <%s! Learn_components.book_recommendation
-        (Data.Book.get_by_slug "coq-art" |> Option.get)
+        (Data.Book.get_by_slug "software-foundations-1" |> Option.get)
         ~link:{href = Url.books; title = "See More Books"} %>
       <%s! Learn_components.book_recommendation
-        (Data.Book.get_by_slug "software-foundations-1" |> Option.get)
+        (Data.Book.get_by_slug "mathcomp" |> Option.get)
+        ~link:{href = Url.books; title = "See More Books"} %>
+      <%s! Learn_components.book_recommendation
+        (Data.Book.get_by_slug "programs-and-proofs" |> Option.get)
+        ~link:{href = Url.books; title = "See More Books"} %>
+      <%s! Learn_components.book_recommendation
+        (Data.Book.get_by_slug "coq-art" |> Option.get)
         ~link:{href = Url.books; title = "See More Books"} %>
     </div>
 
@@ -147,10 +153,10 @@ Learn_layout.single_column_layout
   -->
     <div class="grid gap-6 mt-6 lg:grid-cols-2">
       <%s! Learn_components.book_recommendation
-        (Data.Book.get_by_slug "mathcomp" |> Option.get)
+        (Data.Book.get_by_slug "software-foundations-3" |> Option.get)
         ~link:{href = Url.books; title = "See More Books"} %>
       <%s! Learn_components.book_recommendation
-        (Data.Book.get_by_slug "programs-and-proofs" |> Option.get)
+        (Data.Book.get_by_slug "frap" |> Option.get)
         ~link:{href = Url.books; title = "See More Books"} %>
     </div>