I'm fairly ignorant of the details of static analysis, but why is it being done on programs written in C?

Shouldn't they use languages specially suited for this kind of analysis?

I remember learning that stateless programing (ie. functional programming) makes this kind of analysis several orders of magnitude easier since it eliminates coupling and control flow dependence. Yet I've never heard of critical software being written in Haskell or whatever.

When you're writing safety-critical code, what you want above all else is lack of surprises. Sure, C has pitfalls, what language doesn't? But we know what the pitfalls are. We have decades of experience in avoiding them. The toolchains are mature and very well tested. The source code maps fairly directly to the hardware. You don't have to put your trust in esoterica like trying to find a garbage collector that claims to be able to meet real-time constraints and then trying to understand the edge cases in the analysis on which that claim is based.

It's okay to have bleeding edge technology in the ancillary tools like the static analyzer. But for safety-critical work, you don't want bleeding edge technology in the language in which you're writing the actual code.

Also, a straightforward mapping from source code to machine code is important for auditing generated code.

C99 with some restrictions isn't actually that big a language, it's quite possible to put together a formal semantics for it, especially if you disallow heap allocation.

There's at least one fairly mature implementation of a certified compiler out there (CompCert) with only minor restrictions to the language.

I suspect the arrow of causality goes the other way: the control software was written in C first. Later, Airbus wanted to gain confidence in its correctness.

In other words, the static analysis works on C programs because there are more extant (and mission-critical) C programs than Haskell ones, and the authors of the static analysis software wanted their tool to be as useful as possible, so they chose to analyze C.

If I had to guess, it's because C lets them model their software closely to how the hardware is designed.

Not that much, if any, real-time software written in Haskell, on account of the runtime not being amenable to real-time constraints. And anyway, I suspect it's an industry where "let's rewrite it from scratch" is not something you hear very often.

Yes, you could, but chances are that the provable upper bounds on memory usage or execution time are orders of magnitude above what you think it should take. Anything that produces a new value where you cannot prove that another value becomes unreachable (in which case the compiler could translate it to a destructive update) could trigger a garbage collection that might write half a GB of memory and takes .1 of a second (numbers may be realistic, but if they are, it's pure luck)

Sure.. a garbage collector would mess you up, but garbage collection isn't an intrinsic property of stateless languages.

EDIT: Seems I'm wrong http://www.haskell.org/haskellwiki/GHC/Memory_Management

It is not intrinsic, but hard to avoid. Alternatives include:

- just allocate, never collect (not infeasible with 64-bit memory spaces, if you have lots of swap and can rebozo fairly frequently, but bad for cache locality)

- garbage collect at provable idle times. Question is: when are those?

- concurrent garbage collect, and proof that it can keep up with allocations

Finally, you could try and design a language where one can (often) prove that bar can be mutated in place in expressions such as

    bar = foo(bar,baz)

(That's possible if you can prove there's only one reference to bar at the time of the call)

(Rust's memory model may help here)

I am not aware of any claims that it is possible to write meaningful systems based on this model that do not have to allocate new objects regularly. Problem is that, to guarantee the 'one reference' property, you have to make fresh copies of objects all the time, and that beats the reason why you want that 'one reference' rule.

Thank you for the explanation. That's a lot to think about.

Um, no you can't. Garbage collection and laziness both completely destroy the ability to guarantee runtimes for functions.