[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: GNUism in groff tests, was: pic anomalies

From: G. Branden Robinson
Subject: Re: GNUism in groff tests, was: pic anomalies
Date: Sat, 4 Jan 2020 08:35:17 +1100
User-agent: NeoMutt/20180716

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

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.


[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.  :)

Attachment: signature.asc
Description: PGP signature

reply via email to

[Prev in Thread] Current Thread [Next in Thread]