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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,f3bebae566a54cab X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!news2.google.com!goblin3!goblin1!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Some exciting new trends in concurrency and software design Date: Thu, 23 Jun 2011 14:20:44 +0200 Organization: cbb software GmbH Message-ID: <10s3okv9rjfm8.jkeunop8t1vf$.dlg@40tude.net> References: <8a5765ba-622a-42cd-9886-28ed7cfed31e@s17g2000yqs.googlegroups.com> <4dff5be5$0$6565$9b4e6d93@newsspool3.arcor-online.net> <9b65f3c7-caee-440f-99ed-0b257221ce58@m24g2000yqc.googlegroups.com> <1v2auyktde5q4.1wqpdg3fval5k.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 8bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: g2news2.google.com comp.lang.ada:20988 Date: 2011-06-23T14:20:44+02:00 List-Id: On Thu, 23 Jun 2011 12:57:49 +0200, Yannick Duch�ne (Hibou57) wrote: > Ignoring things can help. > > There is always some stage where you ignore some one of some other things. Yes, but you should not forget that you deal with a model. Many approaches claiming themselves mathematically puristic suffer this error. > FP is less executable than Ada, so there are things you will less bother > with FP, you will be required to bother about with Ada. Do you mean that FP programs are never intended to be executed? (:-)) > Do you see what I mean ? No, I suppose you mean that FPL are more declarative than Ada. That is not necessarily true, because Ada as a language supporting OO decomposition has much declarative stuff to support this, missing in the languages oriented on procedural decomposition. > By the way, if you want to prove an Ada program, how do you do it, if not > by turning it into a view where it is all made of expressions (with > possibly multiple expressions at some point, for coverage) ? Again, if you mean that any formal proof has to be strictly declarative (assuming its relation to the run time). Yes it evidently has to be. But the proof is not the program itself. They are written in different languages of different power. IMO, it is fundamentally impossible to melt them into one. Also consider what would happen if you wanted to prove the proof. You would need a third language for which the second one would be "executable," and the inference it does would be just a program. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de