An Introduction to the Tauto Programming Language

Learn Tauto, a language for writing programs and proving their properties, in 24 chapters: from values and functions to ownership, algebraic effects, dependent types, and theorem proving.

1. The Tauto Language
2. Your First Program
3. Values, Variables, and Basic Types
4. Functions and Control Flow
5. Structs, Enums, and Pattern Matching
6. Lists, Generics, and Type Classes
7. The Four Ownership Kinds
8. Borrowing and References
9. Understanding Algebraic Effects
10. Resumption Counts and Ownership
11. Setting Execution Limits
12. Projects, Tests, and Tools
13. Your First Proofs
14. Proving Equalities
15. Induction and Recursion
16. Tactics and Proof Steps
17. Dependent Types and Universes
18. Case Study: Correct Sorting
19. Case Study: State Transitions and Invariants
20. What Is Guaranteed, and What Is Not
21. What to Build Next
22. Appendix A: Syntax Quick Reference
23. Appendix B: Exercise Hints and Answers
24. Appendix C: Glossary and Learning Checklist