> how do we know the example TCP RFC English Language description isn't logically flawed? They'll surely have needed to translate the English specification int

> how do we know the example TCP RFC English Language description isn't logically flawed? They'll surely have needed to translate the English specification into a formal specification. That act of translation isn't itself a formal process, so it's subject to errors, and also subject to dispute in case of ambiguities or underspecification or contradictions in the English text. You can never formally prove that an informal natural language specification corresponds to a formal specification written in a formal language (although you could try to take another abstraction step by writing a formal grammar and formal semantics for the natural language and then claiming that the interpretation of the natural language text, under that interpretation, agrees with your formal specification... I don't believe this is common or likely to yield useful results unless the natural language text was written in a very controlled way with this kind of application in mind). > On a side note, rather than debating re-writing the Linux kernel in Rust so that it is memory safe(er), why not start working on a formally hardend kernel code? Or does this only apply to logical propositions, e.g. the RFC? Rust's type system can actually be viewed as a formal proof system, where the type checker is verifying proofs about behaviors of the program. But the proofs in question are somewhat weak compared to other formal methods techniques, which can potentially be used to prove stronger claims about program behavior. The Rust ones aren't trivial, though; they rule out quite a few kinds of errors even without having a formal specification for the program's behavior beyond that given by the type annotations. And there are some other features inspired by formal methods, like the fact that match patterns must specify a behavior for every possible value of the expression: https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html Writing formally verified code with a richer specification tool is harder and slower going. Microsoft is paying the equivalent of an academic department (in MSR) to do some of that work. I would hope we would soon see similar stuff in the free software world from a regular academic department at a university... maybe inspired by some of this work from MSR!