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 Path: buffer1.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!us.feeder.erje.net!feeder.erje.net!1.eu.feeder.erje.net!news.swapon.de!eternal-september.org!feeder.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail From: Georg Bauhaus Newsgroups: comp.lang.ada Subject: Re: Build language with weak typing, then add scaffolding later to strengthen it? Date: Tue, 26 May 2015 10:12:22 +0200 Organization: A noiseless patient Spider Message-ID: References: <127b004d-2163-477b-9209-49d30d2da5e1@googlegroups.com> <59a4ee45-23fb-4b0e-905c-cc16ce46b5f6@googlegroups.com> <46b2dce1-2a1c-455d-b041-3a9d217e2c3f@googlegroups.com> <3277d769-6503-4c7f-885f-3a730762b620@googlegroups.com> <3e343282-202d-48e0-b8ab-2f427c1d8c3c@googlegroups.com> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Tue, 26 May 2015 08:11:11 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="b96887e80893c84a90c3007226ca0d1c"; logging-data="22892"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19maaBWaL/PgvoQP5tiViRJ8furRHT6xPE=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.7.0 In-Reply-To: <3e343282-202d-48e0-b8ab-2f427c1d8c3c@googlegroups.com> Cancel-Lock: sha1:IVR2FFUANkIyeNsVzyUbYC3KOfo= Xref: number.nntp.giganews.com comp.lang.ada:193305 Date: 2015-05-26T10:12:22+02:00 List-Id: On 25.05.15 21:54, jan.de.kruyf@gmail.com wrote: > Oberon is very much a reduced instruction set language. Anything complex is either a library package or a code pattern. So formal proof, for those who need that, is relatively easy. Why is formal proof any easier, then? If anything complex is either a library package or a code pattern, then formal proof would have to include these. Patterns are useful, of course, but they do not establish proof by just being patterns? > And for me production-wise it was a big bonus. When you are coding, your immediate working knowledge consists of exactly those 17 pages. How is it that you know the libraries and the code patterns? Can't be from the 17 pages of the report as it mentions none of them. WRT the Ada LRM, this "works" for me: *if* a text book or other introduction(*) or the rationale won't do: employ the structure of the RM: - The core language is text before Annex A. (Some 350 pages) (This would be the equivalent of the Oberon report.) - In there, every section N has a few short paragraphs that introduce the section's topics formally, using definitions. - Many subsections N.M start like the Oberon report, giving grammar; others focus on one subtopic. Note the recurring headings like _Syntax_ for a good guess at where you need to look. > And you know them off by heart in no time, from doing them again and again. Yet what is it that you know from 17 pages? It might feel good, but that isn't good enough for a reference. > And when you do your program design you dont get sidetracked by language complexities. Can we get sidetracked by, say, improper choice of the code pattern? __ (*) http://www.adaic.org/wp-content/uploads/2010/05/Ada-Distilled-24-January-2011-Ada-2005-Version.pdf