Re: Concurrency always is non-deterministic?

[Phil Clayton <phil.clayton@lineone.net>]

On Feb 14, 10:05 am, Erich <j...@peppermind.com> wrote:
> On Feb 14, 2:18 am, Phil Clayton <phil.clay...@lineone.net> wrote:
>
> > functional programming is unsuitable for systems
> > that are any of: real-time, embedded or critical
>
> The first two points, yes, but what about the third. Haven't
> functional programming languages like Haskell been used for critical
> (high-integrity) applications as a substitute for Ada/Spark, because
> they make formal verification very easy?
>
> I'm not claiming it, just believe I've read about it and ask as a
> layman out of curiosity.

Yes, this is worth clarifying.  I am talking about using the output of
a functional language compiler directly in a critical system.  The
main issue (for me) is that the included run-time system is just too
complicated to be trusted.  I'm not sure that it would even be
possible to perform the various verification activities required of a
typical critical system.

Where I've heard about FP used for critical application software, it
is generating code, e.g. C [1].  The risks here are totally different:
we are concerned with the likelihood that an error in the functional
language compiler results in a legal program that is incorrect in a
way that is sufficiently subtle that it is not detected by any
verification activities.  This risk is very small and can be reduced
further by re-running with a different compiler.  This is dwarfed by
the risk due to an error in implementation of the code generation
algorithms.  Functional programming really will help avoid this sort
of algorithmic error: it is especially suitable for data structure
transformation algorithms.  So I believe FP is actually a good choice
for code generators (and verification tools) used in the development
of critical systems.

As for formal verification being very easy.. unless your language is
incredibly simple, it's never easy!  If you know what you are doing,
what slows your formal verification down is usually bad tool support,
rather than the language.  It is usually easier to reason about the
algorithmic behaviour of (purely) functional programs than imperative
programs but it isn't just the programming paradigm that makes a
difference.  For example, justifying algorithmic optimizations often
requires knowledge about ranges of variables, for which Ada types are
incredibly useful because tools can assume values are in their type
range.  Without this, adding/managing such global constraints must be
done manually, which is very laborious.

Phil


[1] Also, I think the languages may be constrained in some way.  (If
your language doesn't have functions as ordinary values, is it still a
functional programming language?)