2 ms·

Formal verification doesn't have to verify the entire functionality of the program to be useful; Rust's type system is supposed to formally verify that your pro

by inigyou 3mo ago

Formal verification doesn't have to verify the entire functionality of the program to be useful; Rust's type system is supposed to formally verify that your program has no memory safety bugs. (It doesn't. Because formal verification is hard. See cve-rs for how to corrupt memory without unsafe. Rust has stated they do not intend to fix cve-rs.)

yencabulator 3mo ago
> Rust has stated they do not intend to fix cve-rs. Huh? That joke repo seemed to ride on https://github.com/rust-lang/rust/issues/25860 https://github.com/rust-lang/rust/issues/25860 which is certainly considered a bug. Here's an actually useful list of known soundness issues, all of which are bugs waiting to be fixed, no stupid snark needed: https://github.com/rust-lang/rust/issues?q=state%3Aopen%20label%3A%22I-unsound%22 https://github.com/rust-lang/rust/issues?q=state%3Aopen%20la...