How to read this book
Tauto Book separates a sequential explanation from reference material you can return to while programming. You do not need to learn proofs first. Start by running a small program, then learn which parts of its behavior to express with types and propositions.
0.1 Three starting points
- Read from the beginning: start at Chapter 1. Use the milestones below, chapter exercises, and your own code to check your understanding.
- Look up a rule: use the language reference index for types, ownership, effects, proofs, and their boundaries. Use the syntax quick reference when you only need to recall notation.
- Diagnose a program: use the execution and verification guide to separate type checking, proofs, execution, and backend failures.
These pages are reading material. They do not edit or recheck code in the browser, or save learning progress. Try examples in the Playground or with your local CLI.
0.2 A sequential course
| Chapters | Prerequisites | Outcome | Check for yourself |
|---|---|---|---|
| 1–2: First execution | No programming experience required | Create a file and inspect its output | How does changing an input or constant change the result? |
| 3–6: Data and functions | Run a first program | Combine branches, records, enums, lists, and generic functions | Can you handle empty data, both branches, and the end of recursion? |
| 7–8: Rules for using values | Functions and data structures | Read APIs in terms of ownership and borrowing | Can you explain moving a value and using it after a borrow ends? |
| 9–11: Effects and budgets | Ownership and borrowing | Separate effect requests from handlers; read continuation and budget constraints | Which effects remain unhandled, and what happens when a budget is exhausted? |
| 12: Projects | A small executable program | Split files and distinguish testing from checking | Have you mistaken displayed output for an assertion? |
| 13–17: Proof foundations | Functions, types, and match | Read propositions as types; use equality, induction, and dependent types | Can you explain the assumptions and conclusion of each theorem? |
| 18–20: Building guarantees | Proof foundations | State algorithm and transition properties and identify their boundaries | Does the executable call the same function that was proved? |
| 21: The next program | Distinguish checking from execution | Design a small practical program with an explicit external boundary | Which I/O and backend behavior needs tests? |
Do not feel obliged to read every chapter at the same pace. Experienced programmers can run the examples in Chapters 1–6 before focusing on ownership in Chapter 7. If you start with proofs, first review match in Chapter 5, type parameters in Chapter 6, and the checking commands in Chapter 12.
0.3 Completing a chapter
- Keep the example's filename and imports when running it. Later blocks with the same filename may continue the earlier blocks.
- Change one input and predict the result before running it.
- Try the exercise and compare with the hints and answers. Explain why the answer works, rather than only reproducing it.
- Use the glossary and checklist to find terms you cannot yet explain and revisit their chapters.
- In proof chapters, strengthen the conclusion or remove an assumption and check what still works. A remaining hole is not a completed proof.
0.4 Reading example results
An example result is a record obtained with a particular CLI when the site was generated. It is neither a fresh run in your environment nor a compatibility guarantee across every backend. Deliberately failing examples and examples with proof holes are labeled with those states.
skipped classifies a declaration as outside the proof kernel. It means neither that all executable-program checks were skipped nor that execution succeeded. Check types, propositions, tests, and runtime results separately.
0.5 Scope and specification
This book is an explanation and a starting point for reference, not a complete normative specification or a promise of future syntax. Proposed designs must be distinguished from implemented and checked syntax. When an example fails, record the CLI version, complete file, command, and diagnostics, then use the verification guide to isolate the problem.