Airbus has been one of the success stories commonly told by the static analysis community:
(Here I mean https://en.wikipedia.org/wiki/Static_program_analysis , not https://en.wikipedia.org/wiki/Static_analysis )
(Here I mean https://en.wikipedia.org/wiki/Static_program_analysis , not https://en.wikipedia.org/wiki/Static_analysis )
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.
There's at least one fairly mature implementation of a certified compiler out there (CompCert) with only minor restrictions to the language.
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.
What are basing that on?
A stateless side-effect free language would be significantly more amenable to real-time constraints b/c you can guarantee run-times for your functions.
EDIT: Seems I'm wrong http://www.haskell.org/haskellwiki/GHC/Memory_Management
- 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)
(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.
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.