[SystemSafety] C for OSs

[Olwen Morgan]

Oh, what a beautiful reflection of the differences of opinion that C and 
C++ engender!

Like my differences with Rod Chapman, my differences with David are also 
long-standing and eminently civilised. I agree that a small subset of 
C++ is superior to C, if only because it gives you the same capability 
(plus-or-minus a bit) that you have in Ada packages. ...

... but, very soon after I encountered C++, I decided that it was such a 
badly designed and badly defined language that I would ever after avoid 
it like the mother of all plagues. This was largely because of the 
messes of poor coding that I occasionally got involved in sorting out.

Naturally, I have a paranoid-critical style of using C++ if I absolutely 
have to (and here the surrealist overtones are even more apt ;-). 
Nevertheless, my instincts are always to use the simplest language that 
I can make to do a job well - which is why, where a C-like language is 
unavoidable, I code in C unless C++ is forced on me (under spectacularly 
ungraceful protest). Another reason is that I feel very exposed coding 
in C++ without decent tools - which cost megadosh ... or at least, tens 
of kilodosh.

Curious how different people have different approaches to dealing with 
cr at p languages. Though I warm to what David has done with eCv, I remain 
unable to shake off my ingrained obsessive Ockhamism.

Olwen ... :-))


On 09/09/2019 11:48, David Crocker wrote:
> Roderick, shame on you for writing in C! A small subset of C++ is vastly
> superior. You get encapsulation, a stronger type system, and generics.
> With generics you can define your own array types (or use std::array if
> it meets your requirements) and bounded string types. You can also
> define your own range-limited scalar types (or with eCv/eCv++ you have
> the constrained typedef in the language already).
>
> David Crocker, Escher Technologies Ltd.
> http://www.eschertech.com
> Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486
>
> On 09/09/2019 10:29, Roderick Chapman wrote:
>> On 08/09/2019 18:23, Olwen Morgan wrote:
>>> Rod Chapman and I have a long-standing (and exceedingly civilised :-)
>>> difference of opinion in this area. If you have the right tools, and
>>> if you are prepared to observe draconian coding discipline, then I
>>> believe that you can in C approach a SPARK Ada level of code quality.
>>> Rod, if I am not traducing him, has lingering doubts about this. IMO
>>> tools are no longer the problem since those who write them simply
>>> retrofit sensible formal semantics to (annotation-extended subsets
>>> of) C and then perform verifications accordingly.
>> I still have reservations. The big challenge is to come up with a
>> formal semantics that is implemented by both your favourite
>> verification tool and all versions of all compilers that you might
>> have to use during the lifetime of a project. If you can "lock in" to
>> exactly ONE compiler, then things are significantly simpler... but
>> this is not a good place to be when, in twenty years time, you really
>> do have to change compiler for a hardware update or some other reason,
>> but the vendor has long since gone out of business. I see far too many
>> projects stuck in this particular rut.
>>
>> In SPARK, it works by the complete removal of undefined behaviours and
>> any dependence on unspecified behaviour. This requires subsetting and
>> forms of analysis, which you need to be demonstrably sound and
>> efficient enough to scale up to large programs.
>>
>> I am currently engaged in writing some highly critical C code, using
>> the latest Frama-C toolset. I find the experience rather
>> frustrating... the problem seems to be two-fold:
>>
>> 1. C is lacking some fundamental features that make SPARK work. (The
>> short version: user-defined scalar types, named type equivalence, a
>> first-class Boolean type, packages, formal parameter modes, and
>> first-class array types).
>>
>> 2. Some very basic things in C are undefined. Worst-offender: signed
>> integer overflow.
>>
>> The upshot is that I find it's very hard to get to an acceptable
>> false-positive rate from the Frama-C WP tool. On a recent SPARK
>> project, the "acceptable" false alarm rate for type-safety proof was
>> ZERO.. so perhaps my expectations are set too high?
>>
>> Example: in SPARK, we use user-defined scalar types all over the place
>> to describe invariants from the problem domain which apply to every
>> parameter, constant and variable of each type. That info is used by
>> the VC generator to constrain the values of variables, so that proving
>> non-overflow becomes tractable. I don't know how to do that in C...
>> (if anyone does know how, please help me out...)
>>
>>   - Rod
>>
>>
>>
>>
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>> Manage your subscription:
>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety