From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,590b710e61b9ddf8 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Received: by 10.68.74.201 with SMTP id w9mr12793253pbv.0.1329231626953; Tue, 14 Feb 2012 07:00:26 -0800 (PST) Path: wr5ni24370pbc.0!nntp.google.com!news2.google.com!postnews.google.com!m7g2000vbw.googlegroups.com!not-for-mail From: Phil Clayton Newsgroups: comp.lang.ada Subject: Re: Concurrency always is non-deterministic? Date: Tue, 14 Feb 2012 07:00:26 -0800 (PST) Organization: http://groups.google.com Message-ID: <073f6ec3-aad8-411c-94ec-9a35276ded97@m7g2000vbw.googlegroups.com> References: <3721724.784.1329154891821.JavaMail.geo-discussion-forums@pbcwt9> <6f19eaa9-c75f-4fca-86d4-bfaee2f51db7@k40g2000yqf.googlegroups.com> <0dbc36f5-15f6-4b47-808c-d19d5ac72cba@x19g2000yqh.googlegroups.com> NNTP-Posting-Host: 2.27.135.203 Mime-Version: 1.0 X-Trace: posting.google.com 1329231626 18636 127.0.0.1 (14 Feb 2012 15:00:26 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 14 Feb 2012 15:00:26 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: m7g2000vbw.googlegroups.com; posting-host=2.27.135.203; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 X-Google-Web-Client: true X-Google-Header-Order: HUALENKRC X-HTTP-UserAgent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0) Gecko/20100101 Firefox/10.0,gzip(gfe) Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2012-02-14T07:00:26-08:00 List-Id: On Feb 14, 10:05=A0am, Erich wrote: > On Feb 14, 2:18=A0am, Phil Clayton 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?)