Explores how adding assumptions to software properties makes those properties logically weaker, using the implication operator from formal logic. Covers three reasons why assumptions are sometimes necessary: when the strong property is impossible to satisfy (e.g., fairness in formal methods, Rust's memory safety guarantee), when satisfying it isn't worth the cost, and when it's not easily verifiable (e.g., mocking APIs). Also observes that most assumptions stem from exoprogram factors like user input, hardware, or third-party dependencies, and that verifying assumptions often requires different tools than verifying the code itself.
2 Impressions