My point is that only works if you’re writing the entire software stack. The moment you rely on someone else’s library, whether it’s to read from a file descrip

My point is that only works if you’re writing the entire software stack. The moment you rely on someone else’s library, whether it’s to read from a file descriptor, a libc wrapper around an OS SYSCALL or whatever, you’re opening up your program to unexpected behaviour. And that’s not even taking into account the slew of very real software bugs that can be introduced from unexpected hardware behavior. Using formal method might prove your applications logic but it doesn’t prove a buffer overflow bug in a library you’ve used, or the OS you’re running on, or the compiler you’ve used from introducing a bug, nor even the hardware itself. Computers these days are sufficiently complex and with enough abstractions that there’s no such thing as a guarantee.