At 2020-01-03T12:45:22-0500, Doug McIlroy wrote: > > C is one of the worst possible foundation languages conceivable for > > automated formal verification > > Yet the Mars rovers run on a wholly checked code base written > in C, subject to certain mechanically enforced restrictions on > coding style.
I did not know that! Thank you--I'm going to go learn about it. > I'm not aware of comparably challenging systems having been verified > regardless of programming language. There is the seL4 microkernel[1], which is written in C and available for several processor architectures (Intel x86, AMD 64, RISC-V [hooray!], and several ARM chips). A debugging build I made in December is about 20k lines before the preprocessor runs and about 30k afterwards. The formal verification code, written in Isabelle/HOL[2], is about an order of magnitude greater than that. I can't address the question of a comparable challenge because I don't know what sort of definition of "challenging" you have in mind. I would, however, defend seL4 against a charge of triviality. :) I once asked why seL4 was written in C instead of a more careful, more strongly typed language. I would have chosen Ada at the time of its initial implementation, and either Ada or Rust today. It turns out I already knew the answer, with a sense of dread: you just can't get traction, especially among non-academic software practitioners, in systems software unless your implementation is in C, or maybe C++ (and less so the latter as the elephant in the room has slowly become acknowledged--see below). That projects like seL4 and CompCERT have happened is heroic; much effort in overcoming the looseness of C has been put into them, not for technical reasons but because of hidebound conservatism in the industry. So yes, on the one hand I complain about rock stars and cowboys slapping together rickety demoware in the language du jour and on the other hand I gripe about there being a lack of linguistic diversity in the industry. I reconcile these grievances by observing that what is missing is a _considered_ evolution from C to some successor that would support the kinds of safety and correctness that Ada or Rust afford. But everyone knows what would happen if a "considered evolution" were attempted; it would be ignored by major industry players until it withered, and if it refused to wither, it would be co-opted[4]. C++ has crumbled under the weight of countless features and due to its size and the combinatorial explosion of interactions of those features is an unmasterable language; Objective-C has been in practice a wholly-owned subsidiary of a single company for many years now; Java shifted from one trait to the other and back; and C# is a remarkable attempt to combine both. So please understand that while I make critiques of C, I try to do so in a measured way. Of C, I would say what Tony Hoare said of Algol, but in a softened form: C was an improvement on nearly all of its predecessors and most of its successors. To bring this back around to groff, the bits of it that are written in C++ are written is a limited dialect of it, largely due to age. I think this is a positive virtue that we should preserve. Conservatism/inertia have served us well here; I'm not a revolutionary about everything. :P > But I stray far from groff. Perhaps--but experts (you) and aspiring experts (like me) sharing domain knowledge about how to get from where we are to the next great breakthrough in software engineering is something that any code project can benefit from. Admittedly, since groff has to interpret a Turing-complete language whereas an OS microkernel and a Mars rover (I suppose) do not, there is a hard limit on what we can verify. But to paraphrase a Debian colleague, that we can't prove that a program halts doesn't mean we can't prove valuable things about programs on the assumption that they _do_ halt. Regards, Branden [1] https://sel4.systems/ [2] https://isabelle.in.tum.de/ [3] http://compcert.inria.fr/ [4] Similarly, you can look at the list of "platinum members"[5] of the Linux Foundation and identify the fingerprints that have made the world's most famous and popular copylefted project effectively BSD-licensed. Anti-copyleft partisans in the community seem largely to not even recognize that they won this war; perhaps they require the assignment of Linux's copyrights to UC Regents to feel that justice has been done. Or maybe the Apache Software Foundation. Or Oracle. :) [5] https://www.linuxfoundation.org/membership/members/
signature.asc
Description: PGP signature
