7

So, as stated on wikipedia:

Lustre is a formally defined, declarative, and synchronous dataflow programming language for programming reactive systems. It began as a research project in the early 1980s. A formal presentation of the language can be found in the 1991 Proceedings of the IEEE. In 1993 it progressed to practical, industrial use in a commercial product as the core language of the industrial environment SCADE, developed by Esterel Technologies. It is now used for critical control software in aircraft, helicopters, and nuclear power plants.

I'm wondering why are languages like this used for critical control software, and why are they developed. For example, can it be written in C?

Why is there need to design this type of specific languages? Because they are "faster" or because they are strictly designed for the system in which they are?

9

why are languages like this one (Lustre) used for critical control software.

Because some software tools (or even methodology) can help in partially proving the correctness of the code w.r.t. some formalized specifications, and because some other (or same, e.g. SCADE) software tools can generate some C code (which would be "safer" and perhaps faster than what hand-written code can realistically achieve) from Lustre source.

Read about static source program analysis.

Notice that some tools exist to help prove that some C programs (with a restricted coding style) are somehow "safe" or "correct" w.r.t. some formalized specification; e.g. look into Frama-C.

Also, recall that some programming languages subset (e.g. most of Ocaml, thanks to it type system, but without its infamous Obj.magic trick) can "guarantee" by design that your program won't crash (w.r.t. some hypothesis).

But remember: there is No Silver Bullet: Because of undecidability of the Halting Problem, you cannot hope proving entirely any software (and you cannot hope formalizing entirely its specification and its environment; you need to accept that software are abstractions ...)

Read also Lattner's blog: What Every C Programmer should know about Undefined Behavior

BTW, several industries (including nuclear, aircrafts, and even health devices etc...) have their specifications and regulations regarding safety critical software. For example DO-178C for the commercial aircrafts. In such cases, software costs a lot more (e.g. per line of code) than your usual phone application, and the software development methodology is very different (and much more bureaucratic: you'll document and need to have formally accepted and tested any change, even a single line patch).

  • 3
    i'm not sure if the halting problem is an issue for these formally proven languages, aren't they usually not turing complete specifically so halting can be decideable? – jk. Aug 24 '16 at 9:23
  • IIRC, Lustre is practically Turing complete, at least because you could embed chunk of C code in it. But I forgot the details and could be wrong. – Basile Starynkevitch Aug 24 '16 at 9:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.