Tris explains how his university training in formal methods (Z, ACL2, etc.) gave him confidence in proving safety‑critical systems, but he found those techniques too heavyweight for everyday web development. After searching for a compromise, he turned to Rust, which offers many of the guarantees of formal methods—especially functional purity and side‑effect control—while remaining practical for general programming. He highlights Rust’s const functions as a compile‑time‑pure construct that enables reasoning, caching, and parallelism, noting their limits (no I/O, mutable state, etc.) and the escape hatch provided by compile‑time macros. Overall, Rust’s type system and language design already enforce much of the purity that formal methods aim for, giving Tris the safety he seeks without sacrificing usability.
1. Tris is the speaker presenting the video.
2. Tris studied formal methods at university, including the languages Z, B, ACL2, and systems such as pacemakers, autopilots, and hospital ventilators.
3. Formal methods are expensive, require unusual external verification languages, and slow down iteration for web and application developers.
4. After graduating and taking a web development job, Tris despaired that the safety guarantees of formal methods were not available to him.
5. Tris posted a question on Stack Overflow that became one of his most popular posts.
6. Tris later found Rust after previously trying Pascal.
7. The video script, links, and images are part of a markdown document freely available on GitHub under a public domain license.
8. Tris recommends learning the basics of Haskell (referred to as HLL) to teach functional programming quickly.
9. Haskell provides features that give confidence similar to formal methods, one of which is functional purity.
10. The factorial function shown is a pure function because its signature contains no IO, indicating no side effects.
11. The main function prints to the screen, so it must have IO and therefore is not pure.
12. Pure functions exhibit referential transparency: calling them with the same inputs always yields the same output.
13. Referential transparency enables predictable caching of return values and easier debugging.
14. Pure functions allow perfect parallelization because their output depends only on their inputs.
15. Rust’s first compiler was written in OCaml, reflecting its functional ML roots.
16. Rust’s const functions can be executed at both compile time and runtime.
17. Const functions differ from Rust macros, which run only at compile time and can perform arbitrary code generation.
18. Const functions have access to a limited subset of Rust, including arithmetic on integers and floats, tuple creation and indexing, array creation and slicing, struct creation, closure expressions without capturing shared borrows (except borrowing values with interior mutability), casting except to memory addresses, calling other const functions, and loop constructs (while, while let, if, if let, match) and range expressions.
19. Const functions cannot use mutable references, interior mutability, string comparison, full floating‑point support, iteration without a crate, printing (IO), or reading environment variables.
20. Const functions can call other const functions.
21. Because IO functions cause side effects, they cannot be called from a const function.
22. Debugging const functions is limited to examining the return type or triggering a compile‑time panic or failed assertion.
23. The const Panic crate provides const versions of assertions that panic with an error message and variables.
24. Rust macros can execute arbitrary code at compile time and insert the results as potentially const values, serving as an escape hatch for const functions.
25. Rust’s language design encourages immutability unless mutability is explicitly opted in, which is signposted in function signatures.
26. Global state is deliberately discouraged by Rust’s language and ecosystem.
27. Rust promotes side‑effect‑free patterns and functional/reactive programming through its type system.
28. Rust’s type system encodes side effects, allowing the compiler and crates like Rayon to reason about parallel code without a restrictive purity system.
29. Rayon can turn ordinary iterators into parallel iterators with a single line change to existing code.
30. Const functions in Rust are not pure in the strictest sense but are practical; Rust aims to be as pure as possible without sacrificing practicality.