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

Speaker Intro
讲者简介

• Principal Firmware Architect in Microsoft SCHIE (Silicon and Cloud Hardware Infrastructure Engineering) team
  微软 SCHIE 团队首席固件架构师。
• 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 Patterns 负责讲清 trait、关联类型、类型状态这些机制本身，而这本书要讲的是：如何把这些机制真正落到硬件诊断、密码学、协议验证和嵌入式系统这些真实领域里。

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
Correct-by-Construction 光谱

← 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?    Won't compile.
Crashes in prod.    Fails in CI.      Fails in CI         Never exists.
                                      (probabilistic).

This guide operates at the rightmost position — where bugs don’t exist because the type system cannot express them.
这本书关注的就是最右边那一端：错误之所以不存在，不是因为测出来了，而是因为类型系统根本不允许它被表达出来。