fixes

BlastWind · Jan 2, 2025 · e50fc26 · e50fc26
1 parent 911734d
commit e50fc26
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 10 deletions.
diff --git a/book.toml b/book.toml
@@ -3,7 +3,7 @@ authors = ["blastwind"]
 language = "en"
 multilingual = false
 src = "src"
-title = "A Tour of Formal Verifications"
+title = "A Journey Through Formal Methods"
 
 [output.html]
 mathjax-support = true
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
@@ -1,5 +1,5 @@
 # Summary
-
+[Introduction]()
 - [Foundations](./foundation.md)
   - [Glossary]()
   - [Paradoxes]()

diff --git a/src/foundation.md b/src/foundation.md
@@ -1,4 +1,6 @@
-# Outline
+# Foundations
+
+## Outline
   - Glossary: Introduce terms, reference later
   - Paradoxes: Puzzles to start thinking about that relates to inconsistency and others
   - Incompleteness, Undecidability, Inconsistency: Defining three key terms
@@ -10,15 +12,9 @@
 	- System F and the Polymorphic Lambda Calculus
 	- Modal Logic and Monads
   - HoTT: Topology and type theory?!!
-- [Modern Dependently Typed Languages]()
-  - [Idris](./idris.md)
-- [SMT Solvers]()
-  - [Theory and Implementation](./smt_theory_and_implementation.md)
-  - [Symbolic Execution]()
-
 
 
-# Paradoxes, Foundations, and Computability
+## Uncompiled
 
 1901. Russell's paradox. This is a paradox expressable (encodable) in naive set theory and formal logic.