Certain proofs about a program, implemented using types, are useful in high level programming, as well as low level programming. See Rust in the linux kernel [1

Certain proofs about a program, implemented using types, are useful in high level programming, as well as low level programming. See Rust in the linux kernel [1], and Rust on Android[2]. One way to think about it, is that proofs about a program are a continuum, rather than one or the other. Sure, going all the way, disallowing mutability and requiring types for everything, might make the system more provable, but slower as well. There are some different ways to look at a program: Corporate developer: "Programs are to be run, and occasionally read or proved correctly" Donald Knuth: "Programs are to be read, and occasionally run" Type Theorist: "Programs are to be compiled, and occasionally run or read" https://thenewstack.io/rust-in-the-linux-kernel/ https://thenewstack.io/rust-in-the-linux-kernel/ https://security.googleblog.com/2023/10/bare-metal-rust-in-android.html https://security.googleblog.com/2023/10/bare-metal-rust-in-a...