Re: [Haskell-cafe] Re: Stone age programming for space age hardware?

[Matthias Guedemann]

 Perhaps it's just my lack of imagination that was driving my original 
 question. I'm just having a hard time imagining how to write reasonably 
 interesting algorithms that way.

Very likely they have very specific functionality and hopefully a precise
specification about what to do if the memory bounds are reached (at least some
failsafe mode etc.) Many of these programs are very simple, but deliberately
so.
 
 As I wrote, they might cheat. It's entirely possible to implement 
 dynamic memory on top of fixed-size arrays and use indexes instead of 
 pointers. Of course, I have no idea if that's what they do.

I think it is very likely done that way. I know this kind of programming from
Java-smartcards. These support a subset of Java and allow the creation of 
objects
only when installing a program on the card. There is no garbage collection,
objects are persistent, i.e. creating new objects at runtime would fill up the
available (very low) memory. Dynamic creation is done by reusing one freed
object of the statically allocated ones or returning an error if no free object
is available. 

Systems in high security or safety applications and those with properties like
very low memory, very slow CPUs etc. often have requirements that makes direct
usage of languages like Haskell very difficult or impossible. They are
programmed in a way that makes their behavior as deterministic as possible,
often also from the temporal view. If you have dynamic data structures with
non-O(1) access it is also not possible to guarantee RT bounds.

regards
Matthias
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Stone age programming for space age hardware?

[Matthias Guedemann]

Hi,

 The real reason behind my surprise was, that I was wondering how more 
 modern languages could make inroads into such an environment. Haskell 
 without recursion and dynamic memory allocation? Hard to imagine.

for some safety critical applications that require certification, SCADE with the
underlying Lustre language is used. It has formal semantics and some properties
can be checked with automatic verification (up to linear arithmetic).

The Lustre dataflow programs are then transformed to C (or Ada), by compiling to
automata and representing those in C. This transformation is realized in Ocaml
afaik. I think these kind of transformations, maybe specifying an embedded DSL
instead of using a language like Lustre resulting in C with static bounds
etc. could be a way to use Haskell. But anything using dynamic memory
allocation, GC etc. is dangerous for real-time bounds. These programs also often
run on old outdated, but reliable HW for which mainly C compilers exist. The 
used standards only allow a certain set of programming languages (or subsets of
these languages) and you even have to use proved and tested compilers and
tools. 

 I have a hunch that the real restrictions of this kind of software are 
 not concerned with fixed memory, iterations, whatever, but rather with 
 guaranteed bounds. If that is indeed the case, how feasible would it be 
 to prove relevant properties for systems programmed in Haskell?

I think proving the correct transformation of some input language to static C
using Haskell is possible. Functional languages like Haskell or Ocaml in the
case of SCADE are well suited to this, due to lack of loops, side effects etc.

I think atom is such a DSL embedded into Haskell that can generate code for
real-time systems.

regards
Matthias
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe