Type-Driven Correctness in Rust / Rust 中的类型驱动正确性

Speaker Intro / 讲师简介

• Principal Firmware Architect in Microsoft SCHIE (Silicon and Cloud Hardware Infrastructure Engineering) team / Microsoft SCHIE（Silicon and Cloud Hardware Infrastructure Engineering）团队首席固件架构师
• Industry veteran with expertise in security, systems programming (firmware, operating systems, hypervisors), CPU and platform architecture, and C++ systems / 在安全、系统编程（固件、操作系统、虚拟机监控器）、CPU 与平台架构以及 C++ 系统方面经验丰富
• Started programming in Rust in 2017 (@AWS EC2), and have been in love with the language ever since / 2017 年在 AWS EC2 开始使用 Rust，此后长期深度投入

A practical guide to using Rust’s type system to make entire classes of bugs impossible to compile. While the companion Rust Patterns book covers the mechanics (traits, associated types, type-state), this guide shows how to apply those mechanics to real-world domains - hardware diagnostics, cryptography, protocol validation, and embedded systems.

这是一本关于如何利用 Rust 类型系统，让整类 bug 在编译阶段就无法出现 的实用指南。配套书籍 Rust Patterns 讲解了相关机制（trait、关联类型、type-state），而本书则聚焦于如何把这些机制 应用 到真实领域中，例如硬件诊断、密码学、协议校验与嵌入式系统。

Every pattern here follows one principle: push invariants from runtime checks into the type system so the compiler enforces them.

本书中的每个模式都遵循同一个原则：把原本依赖运行时检查的不变量推进到类型系统中，让编译器来强制保证它们成立。

How to Use This Book / 如何使用本书

Difficulty Legend / 难度说明

Pacing Guide / 学习节奏建议

Annotated Table of Contents / 带说明的目录

Prerequisites / 前置知识

The Correct-by-Construction Spectrum / “构造即正确”光谱

Less Safe                                                    More Safe

Runtime checks      Unit tests        Property tests      Correct by Construction
----------------    ----------        --------------      -----------------------

if temp > 100 {     #[test]           proptest! {         struct Celsius(f64);
  panic!("too       fn test_temp() {    |t in 0..200| {   // Can't confuse with Rpm
  hot");              assert!(          assert!(...)       // at the type level
}                     check(42));     }
                    }                 }

Invalid program?    Invalid program?  Invalid program?    Invalid program?
Crashes in prod.    Fails in CI.      Fails in CI         Won't compile.
                                      (probabilistic).    Never exists.

This guide operates at the rightmost position - where bugs don’t exist because the type system cannot express them.

本书聚焦于最右侧的那一端：bug 之所以不存在，不是因为它们被测试捕获，而是因为类型系统 根本无法表达这些错误程序。