221–225 of 225 posts
Earlier quoted context omitted.
Sel4 would like to have a word. Inb4 you move the goalposts for "at scale". This is an operating system with capability-based access control which is not something that most operating systems even have. Also the cryptographic constraints are part of the proof system.
I'm not sure Sel4 can be considered "at scale", given the rather extreme amount of effort that went into it.
Earlier quoted context omitted.
And yet C code runs the world. You might be right in theory but in practice C is the most successful programming language in history. At work we routinely deploy million+ lines of C in production running large international airlines and airports. And it works.
Historical accident, due to UNIX winning out the server room. In early 1980's it was only running Bell Lab's world and a couple of universities that got hold of the source tapes.
Earlier quoted context omitted.
And yet C code runs the world. You might be right in theory but in practice C is the most successful programming language in history. At work we routinely deploy million+ lines of C in production running large international airlines and airports. And it works.
that C code is prolific is a historical fact, it does not imply anything about efficacy or soundness "it works" is factually not true, look at ~any CVE
Earlier quoted context omitted.
And yet C code runs the world. You might be right in theory but in practice C is the most successful programming language in history. At work we routinely deploy million+ lines of C in production running large international airlines and airports. And it works.
that C code is prolific is a historical fact, it does not imply anything about efficacy or soundness "it works" is factually not true, look at ~any CVE
Earlier quoted context omitted.
that C code is prolific is a historical fact, it does not imply anything about efficacy or soundness "it works" is factually not true, look at ~any CVE
No successful software is bug free. Except for proven correct code like CompCert and seL4 of course.