Hacker News Reader

Comment by pooriaazimi | Hacker News Reader

Very true.

But in some cases, you simply can't use something like C. A friend of mine is currently trying to write a microkernel and mathematically prove that it's 100% bug-free (similar works on the L4 microkernel: [1] and [2], though they might not be the best articles on this matter as I just found these links with a quick Google search). He uses Haskell and ML for this project (He'd use Ada, but he already knows some Haskell and ML and doesn't want to re-learn everything).

[1]: http://ertos.nicta.com.au/research/l4.verified/

[2]: http://www.linuxfordevices.com/c/a/News/NICTA-sel4-OK-Labs-O...

View on HN

The target code for the seL4 project is actually written in C. They do however use Haskell as a stepping stone (they have an abstract spec of their system, which they then prove is implemented by a Haskell implementation, which is in turn implemented by the C implementation).

Do you have any links to your friends work?

Can your friend prove the Haskell and ML compilers he is using are 100% bug free as well? And the hardware it is running on? (both the compiler and the execution environment if they differ)

If you're interested, the German Verisoft project [1] aims at such pervasive verification. AFAIK they haven't yet verified anything matching the complexity of seL4, but they did verify a simple real-time OS. Of course you do need to stop somewhere, as in trusting something "blindly" (say, the verification tools themselves and the hardware they run on).

[1] http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...

Formal methods != safety-critical.

I think it'd be a hard sell to use ML in safety-critical systems due to the non-deterministic runtime of the GC and potential for memory exhaustion.

As a counter-example, C doesn't prevent formal methods - FWIW VxWorks puts out Arinc 653 and MILS products that are verified* using formal methods.

* - This is carries the following caveat, I believe the core OS is formally verified but the particular BSP/configuration needs be tested/certified by the customer or at the customer's expense.

However, there is a lot of work on generating C code from formal models in Haskell or ML. Verify the high level code; verify the compiler; target a subset of C whose semantics you understand. See e.g. L4; Lustre; Copilot.

IIRC type systems based on linear types are quite promising for making a version of ML without a garbage collector --- there could be some interesting progress here soon!

Being non-deterministic is a non-starter for safety or mission critical systems.

One of the foundational concepts of safety-critical design is strict scheduling of resources. The schedule must be strictly deterministic. The process must get it's work done in the time allocated because the scheduler will move on regardless. It's why you don't do recursion in safety-critical systems. Strictly speaking, you're not even supposed to use while loops in safety-critical systems. In the five years I worked in avionics, the only time I saw a while loop was in code review where the person who wrote it (always a new person) was directed to take it out.

All that being said, safety-critical software production is more about the processes than coding. Even crappy programmers can be taught how to write good safety-critical code when the company adheres to best practices.

As far as the original post, Ada and C. Ada has tremendous support for concurrency and is stable as the day is long. Not much in the way of libraries, but honestly not that important on the kinds of projects you would use Ada to build.

> In the five years I worked in avionics, the only time I saw a while loop was in code review where the person who wrote it (always a new person) was directed to take it out.

I can understand the concern about loop termination, but what is the alternative? Are for loops without a hardcoded upper limit allowed? Or must all loops be unrolled?

Reply on news.ycombinator.com