The Tauto Language
This book introduces Tauto to readers learning its syntax for the first time. Starting with values and functions, you will learn to read and write ownership rules, algebraic effects, dependent types, and theorem proofs. The chapters are intended to be read in order.
You should have used variables, functions, and if expressions in another programming language. You do not need prior knowledge of Rust or formal proofs. It is fine to skim the harder chapters on a first reading.
If time is limited, read Chapters 1–5, then 7–9, then 13–15, and finally Chapter 20. After that, move on to tactics, dependent types, and verified programs.
About this book
The code in the book falls into two categories:
- Small, independent programs: save them to a file and run them. Their code blocks include file names.
- Excerpts: these use standard-library functions, lemmas, or syntax macros and belong in a project that imports those definitions. The book identifies the required imports and definitions from earlier chapters.
The book follows three principles:
- Distinguish running a program from proving it correct.
- Distinguish ownership checking, effects, and the proof kernel.
- Connect what you learn to real programs.
1.1 Start with the idea
Tauto lets you express a program and proofs of its properties in one language. Most of the time you write functions, branches, and data-processing code. Where needed, you can also express a claim such as “this function returns a result with this property for every input.”
The following program shows both sides of Tauto.
import std::Base
let answer := 6 * 7
perform show("answer", answer)
theorem two_plus_two(): (2: Nat) + 2 = 4 {
Refl
}
// The host observes the computed answer; the kernel checks the equality theorem.
✓ theorem two_plus_two : 2 + 2 = 4 answer = 42
The first part computes a value and asks the host to display it through the show operation. Running it produces:
answer = 42
The second part proves that the natural-number expression 2 + 2 equals 4. (2: Nat) + 2 = 4 is not a Boolean value: it is a type to be proved. Check this part with tauto check.
ok answer
ok two_plus_two
1.2 Two layers, one language
Tauto has a layer for ordinary programs and a layer for dependent types, propositions, and proofs. The programming-language part of the former is called Nib.
| Programming layer | Proof layer |
|---|---|
fn, let, var, if, match | theorem, Prop, Eq, inductive |
i64, Text, List(A), Vec(A) | Nat, Type, Type1, dependent types |
perform, handle, ! {effect} | Refl, induction, by rewrite!(...) |
| Evaluators and backends | A small proof kernel |
A program being well typed is different from it meeting the intended specification. The type fn f(x: i64): i64 tells you the input and output types. It does not automatically establish that f sorts its input, is cryptographically secure, or never leaks memory.
1.3 How to read the book
- Part I covers values, functions, branches, data types, and lists.
- Part II covers ownership, borrowing, algebraic effects, execution limits, and project management.
- Part III treats propositions as types and introduces equality, induction, tactics, and dependent types.
- Part IV discusses using proved programs in practice and suggests what to study next.
Think about it: Name three properties of programs you have written that their function types alone do not express.