Ada's formal verification capabilities have fallen behind Frama-C for ANSI/ISO C.
Frama-C allows formal verification of essentially arbitrary heap manipulation algorithms. You can implement linked lists and graphs in traditional C with Frama-C annotations in the comments, then prove your code never dereferences NULL, never has an integer overflow, etc.
One single commercial Ada vendor offers Spark, a formally verifiable subset of Ada. Spark does not allow arbitrary dynamically allocated data structures like Frama-C does.
Strange (but interesting (point of view. I always found Frama-C so verbose where spark has most checks as implicit, and has ways to express not-null pointer as types. I've always found eacsl a pain to write and even more with pointer manipulation.
Spark has added checks on memory ownership, that it seems (willing to be corrected) Frama-C didn't have yet.
From a pure tech stack point of view, down there you'll find Why3 and SMT solvers to perform most automatic proof/discharging of verification conditions, and then around that you'll find either a rich set of plugins (Frama-C) because C is... a tall order, or a series of static analysis tools (heavy-duty like codepeer, or lightweight libadalang-based abstract interpretation things) combined into the proof and verification environment. There's also been a lot of amazing work on floating point code verification for both in the previous years, and it was done mostly at the Why3 and SMT solver (or different kind of solvers/verifiers such as gappa) so everyone profits.
And, lest people might think both communities don't interact, the Spark and Frama-C people have an annual (or is it every other year) joint conference.
I'd be quite happy to find more people diving into Frama-C and see what they do and how they manage to write safe software. I'd also be quite happy to see rust building over Why3 (among other things) for their proof/verification efforts. More fruits from all the deep efforts of the verification community.
'Frama-C so verbose': ??? Ada is the most verbose programming language, ever, even before you had the extremely verbose Spark contracts. Could you show me an example of Frama-C with annotations being more verbose than Ada/Spark?
'Spark has added checks on memory ownership': A Rust-like pointer ownership tester has its advantages and limitations.
Advantages: if you have team of 20 engineers working on a 20 million line web browser and no single engineer understands how the whole code base works, a pointer borrow-checker prevents an important class of errors.
Disadvantages: Rust tutorials point out that you have to resort to 'unsafe Rust' to implement even an intro-to-computer-science linked list. You have to use unsafe Rust to implement your fancy heap manipulation algorithms. Unsafe vs safe Rust is a bit like Ada vs. Spark ("safe Ada").
'I'd be quite happy to find more people diving into Frama-C': Frama-C is trending upward and Ada is in decline, ever since the Ariane 5 explosion on 4 June 1996. The US DOD consequently shut down its Ada office and eliminated the Ada requirement, and C/C++ subsets increasingly dominated.
The verbosity I felt in Frama-C contracts (when I tried back when) e.g. was around C's lack of 'parameter passing intent' specification (Ada has in, out, in out, not just by-value, by-ref, by-constant-ref-but-have-fun-with-the-value. People pass their structures as reference (struct thing *) and you have to ensure everywhere that that pointer isn't null. Same for over/underflow that isn't implicit in C. So lots of things needed to be required/checked explicitly instead of implicitly of with typing in SPARK. Cbmc has a similar thing where it has options to insert check if you ask it, checks that cbmc decides where to put, but are not defined in the language.
As for the rest, I checked again some recent Frama-C examples after your reply and verbosity is on par (similar quantifiers, loop invariants, etc.) and I don't see 'extremely verbose' in neither. Mostly I was focused on implicit versus explicit (in a 'boilerplate' sense).
As for the decline of Ada I see different things in my industry and a language and environment that keeps evolving and getting into more industries and making strides in very interesting domains. The DOD isn't the most interesting indicator of the liveness of a language, and I'm not sure what Ariane 5 brings here, except that when you reuse a binary component in a different setting without integration testing you get wild French fireworks?
As for the 'can't program a basic list in rust' I can only say that 99.9% of the time we're not rewriting a basic data structure, we reuse one from some standard library or a trusted component library, and I may have seen maybe one bug in those in my 15y or sw engineering, and countless ones in app or business logic, or serialization/deserialisation code... So yeah, if rust, spark or other hard ass static analysis tools makers are reading this, please keep making proof & verification tech modular. The more the tech advances the more spark we can have proved automatically without proof chops, the safer the world will be. But let me opt in the very hard stuff, please... Let me put the effort where it counts.
Yes, SPARK has a Rust-like borrow checker that doesn't allow implementing arbitrary pointer graphs. You have to use 'unsafe Rust' to implement linked list containers which, once implemented, other parts of the codebase can then consume in 'safe Rust'. Seems to be the same deal with SPARK ('safe Ada') vs vanilla Ada ('unsafe Ada').
Interestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area.
Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)
Are there vendors who provide support for tool qualification for frama-c? By that I mean documentation support that can be provided as part of the certification process, so when you say "Frama-c verified this code does not contain any arithmetic overflow", it is possible to back that up with "And Frama-c version x.y.z has sound analysis, evidenced by ...."
Great question. C/C++ is definitely trending upward in 'safe software' systems even though it isn't ready and industry as a whole isn't (as far as I know) using Frama-C. Are Tesla/Google/Apple hiring Ada engineers to build the car autopilots that control whether we live or die? Nope, seems to all be C++, God help us all.
With CBMC it's even easier. You don't need magic comments in foreign languages to prove linked lists, arrays, graphs, trees, hashtables, ...
If you need to formalize contracts you do it in C, but rarely need it
Coding is the process of fully understanding what needs to be built. We've all seen architecture astronauts churn out reams of UML that still result in a broken system. Exploring the space via iterative MVP is far more productive.
> Coding is the process of fully understanding what needs to be built.
Not every domain affords you the luxury of coding the wrong thing and then fixing it in a later iteration. Sometimes due to financial constraints, other times because people wouldn't exactly be okay with the 0.7.1 version of your plane software leading to crashes until the next patch.
That said, i somewhat agree with you that UML and abstractions can only lead to problems if there's too many of them. A few high level overview diagrams can be good to have, but only as long as they conform to the actual architecture and models 1:1, and as long as they're not made at the expense of actually writing working software and perfecting it.
However, as long as only one person with incomplete knowledge of the domain or requirements is the one to write the code, you'll still end up with sub par solution. Personally, i think that the only way around that would be a paradigm shift of sorts - instead of planning meetings that aren't good enough, you might as well do programming meetings and mob programming in which you'd code the most important architectural bits of the software that you need, leaving the legwork for individual contributors later.
In my experience, code review is far too late for serious decisions to be made. At best, the reviewer will need to wrangle with hammering your sub optimal code into shape, at worst they'll just be like: "Sure, this looks like Java, it can go into the main branch. QA can figure out whether it's good enough or not."
The best application for formal proof is actually in lightweight sanity checks as opposed to "deep" review of your code. To put it very clearly, it should simply not be possible for a properly-engineered program to conflate feet w/ meters and crash a space probe as a direct result of that conflation. There's just no way that this is ever valid semantics.
interestingly, that's one of the areas where Ada shines, as you can define your own integer subtype that will help you preserve the semantics (and Ada has, iirc, no implicit casts, so it would require explicit cast to push feet into metres (and it might be made so that such cast would actually convert the values properly)
> But when your deployment costs run into the 7 to 10 digit numbers
That's when you throw things into simulation and do some Hardware-in-the-Loop testing. If I learned anything from studying the failure of Ariane V flight 1, it's that while analysis can be useful, testing is usually even better.
Hi, do you have a source for the French nuclear plant use? Some kind of paper? Really interested in real-world applications of Spark and had never heard of such. To me the nuclear world was walled off with very specific tech, different than the stuff from rail or avionics.
I've worked on railway systems, but I didn't use Spark. I've seen many mentions to Spark being used in nuclear power software during conferences and presentations. But I'm afraid open materials might not be available...
Thanks! I know of some rail projects in spark some colleagues worked on (and some internal company recruiting efforts) but I guess it's quite recent and maybe not yet deployed.
Took a university course on it way back. Seemed about as pleasant to use as Pascal, though the ecosystem around ADA felt non existent. Probably better to use it for lower level logic when stability and correctness are the primary concerns.
On the bright side, at least there's an open source compiler available for it as a part of the GNU project: http://www.gnu.org/software/gnat/
I'm sure Ada makes a reliable program, but wouldn't it also be good to have an Erlang/Elixir style "self-healing" system with supervisors that can stop and restart each other?
That actually is done with a lot of these kinds of systems. In many of the ones I've worked on you have software or hardware "watchdog timers" that have to be reset, or a process will be terminated and restarted (how will vary a bit). Hardware watchdog timers usually trigger something like a reboot, causing the program to be reloaded and restarted. That's about the simplest you can make a supervisor, but you can have more complex ones monitoring the actual internals to respond should the state become corrupted in some fashion as well.
The programs that ran on the Apollo Guidance Computer were written this way. If there was a sufficiently bad error, the AGC would restart execution. The programs took advantage of the memory in use at the time being non-volatile, and not reset to zero when the computer restarted, so the program could figure out what the CSM or LM was doing, and continue it.
This actually happened on Apollo 11. The 1201 and 1202 program alarms were the computer overloading, and running out of space for more processes. When this happened, the computer would reset, and navigation would pick up again.
To add to this, usually most of the systems in avionics or support systems on the ground are dual-hardware (when not more). There's lots of work done to ensure there's no single point of failure and hardware (and more and more, software) failures are handled safely. Regulators add every 5-10y some pressure on time-to-recovery and acceptable data of service loss (counted in milliseconds even on ground systems).
Erlang didn't invent much there, and restarting/rebooting isn't always possible (try doing that in less than 10ms). Sometimes, the application itself needs to handle problems. This puts lots of 'classic IT' (interface bonding, fail overs, etc.) stuff to the bin very quick.
I'm not sure that mindset fits for this kind of problem. It's not a web server handling lots of independent requests, it's a real-time critical system that is required to always transition to the correct state within the deadline. I'm no expert on this stuff though.
Ada/Spark can do that too, but you also want things like memory safety, hard real-time and/or constant-time capability, and provable correctness. Ada also enables those capabilities.
I've been looking into erlang on and off for nearly 14 years now. I think the language is really neat. But the self-healing supervisor tree thing is something that I've yet to get my head wrapped around.
Like ... if you have some code that's like "X / 0" then it seems like it's not going to matter how many times you restart the process.
The general strategy is to test the system to the point where any bug like that is an edge case, some weird input you didn’t expect.
So every time you get that input you’ll still crash, but other transactions will continue normally. Hopefully that input is either due to a transitory glitch like a bit flipped in RAM, or a user who isn’t bored enough to keep submitting it, but either way the process isolation means all your other jobs can continue.
I wish I had more opportunity to use Ada. GNAT Studio can be buggy but the language itself and the safety it brings to software engineering is really nice to work with.
Kinda reminds me of the Rational suite of programs from early 2000's that did UML modelling and other aspects of software requirements & project management.
They were some of the buggiest most crash-probe applications I've ever used, whilst the whole time their marketing trumpeted about how much better the quality of your software would be if you used them.
Just a small gripe - this article shouldn't really be "How Masten Space ..." I think that story would be fascinating. This article is more of "Why" and "What" which is still worth reading.
Frama-C allows formal verification of essentially arbitrary heap manipulation algorithms. You can implement linked lists and graphs in traditional C with Frama-C annotations in the comments, then prove your code never dereferences NULL, never has an integer overflow, etc.
One single commercial Ada vendor offers Spark, a formally verifiable subset of Ada. Spark does not allow arbitrary dynamically allocated data structures like Frama-C does.
https://frama-c.com/