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,FREEMAIL_FROM autolearn=ham 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,UTF8 Path: g2news1.google.com!news3.google.com!feeder.news-service.com!94.75.214.39.MISMATCH!aioe.org!.POSTED!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: Some exciting new trends in concurrency and software design Date: Thu, 23 Jun 2011 12:57:49 +0200 Organization: Ada @ Home Message-ID: 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> NNTP-Posting-Host: HfNAdMB88ZE8crK0iV2fMQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org User-Agent: Opera Mail/11.11 (Linux) X-Notice: Filtered by postfilter v. 0.8.2 Xref: g2news1.google.com comp.lang.ada:20015 Date: 2011-06-23T12:57:49+02:00 List-Id: Le Thu, 23 Jun 2011 12:25:00 +0200, Dmitry A. Kazakov = a =C3=A9crit: > This is a weak argument. The strong one is that the mathematical numbe= rs > used in engineering are simply incomputable. The question is not = > efficiency > ("how"), it is "if": you cannot represent numbers involved, e.g. real > numbers. Engineering computations are on the model numbers, where rang= e = > is > just one constraint among others. Was indeed what I wanted to mean (yes, even SML is not able to really = express the ideal nature of numbers, and nothing is able to). > All programming is actually about constraints, which makes things so = > hard, > mathematically, algorithmically and also in terms of types (e.g. LSP > violation). Ignoring this does not help. Ignoring things can help. There is always some stage where you ignore some one of some other thing= s. = This is an unavoidable part of a design or understanding process (either= = with math or computation, this is true with both). The question is: how = do = you forget less and less as the time go, and how do you ensure you do no= t = forget what is relevant for this and that (=E2=80=9Cthis=E2=80=9D and =E2= =80=9Cthat=E2=80=9D don't occur = at the same time). That's why I underlined the matter of focus: Ada and = = SML have different focus. 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. There may be = techniques to make FP more executable (I do not know enough about OCaml = = compilers), but I believe FP is primarily a seed to derive from. If you = = don't expect FP text to be a final release, you can drop some physical = matters at this stage. Let say, if you can execute it, that's for testin= g = and prove by execution, which make it more handy than maths. Do you see what I mean ? By the way, if you want to prove an Ada program, how do you do it, if no= t = by turning it into a view where it is all made of expressions (with = possibly multiple expressions at some point, for coverage) ? That's what= = SPARK do so far. Yes, SPARK include Ada's type constraint in the proof = requirement, so that is not strictly comparable, but this is a matter of= = stage and focus. Let say the functional view you get when proving an Ada= = program with SPARK, is more frozen and narrowed than what an expression = of = the same program would be with SML. And =E2=80=9Cfrozen=E2=80=9D and =E2= =80=9Cnarrowed=E2=80=9D should not = occurs too much early (and can't occur early anyway), and even, you may = = want to keep an hand or an eye on the non-frozen / non-narrowed view at = = any time. Do you feel the picture ? -- = =E2=80=9CSyntactic sugar causes cancer of the semi-colons.=E2=80=9D [Ep= igrams on = Programming =E2=80=94 Alan J. =E2=80=94 P. Yale University] =E2=80=9CStructured Programming supports the law of the excluded muddle.= =E2=80=9D [Idem] Java: Write once, Never revisit