5 ms·

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

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/ http://ertos.nicta.com.au/research/l4.verified/ [2]: http://www.linuxfordevices.com/c/a/News/NICTA-sel4-OK-Labs-OKL4/ http://www.linuxfordevices.com/c/a/News/NICTA-sel4-OK-Labs-O...

thalur 14y ago
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)
- oggy 14y ago
  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.pdf http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...
jbester 14y ago
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.
- dons 14y ago
  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.
- njs12345 14y ago
  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!
- Czarnian 14y ago
  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.
  - cpeterso 14y ago
    > 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?
oggy 14y ago
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?

thalur 14y ago

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)

oggy 14y ago
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.pdf http://www.ertos.nicta.com.au/publications/papers/Klein_08.p...

jbester 14y ago

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.

dons 14y ago
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.
njs12345 14y ago
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!
Czarnian 14y ago
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.
- cpeterso 14y ago
  > 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?

oggy 14y ago

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?