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: a07f3367d7,23c0de5a42cf667e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!216.196.110.149.MISMATCH!border2.nntp.ams.giganews.com!nntp.giganews.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: "(see below)" Newsgroups: comp.lang.ada Subject: Re: GNAT packages in Linux distributions Date: Thu, 27 May 2010 16:21:57 +0100 Message-ID: References: <87mxw9x7no.fsf@ludovic-brenta.org> <16bz9kvbqa8y9$.155ntpwpwl29d.dlg@40tude.net> <4be97bea$0$2966$ba4acef3@reader.news.orange.fr> <1p87qdlnjbufg.127laayhrw9x3$.dlg@40tude.net> <4j73xhgimt6r$.pu55kne2p2w5$.dlg@40tude.net> Mime-Version: 1.0 Content-Type: text/plain; charset="US-ASCII" Content-Transfer-Encoding: 7bit X-Trace: individual.net 93y+5rn1WACe80ESVoh5fQqO6n9mFSeonwgg93SipxRoWnfZ2q Cancel-Lock: sha1:PdBL3iX+MWv71IAo5Gz3NUwkFCo= User-Agent: Microsoft-Entourage/12.23.0.091001 Thread-Topic: GNAT packages in Linux distributions Thread-Index: Acr9sFg9XFP+kyUgHUerY26ow5qLDA== Xref: g2news2.google.com comp.lang.ada:12085 Date: 2010-05-27T16:21:57+01:00 List-Id: On 27/05/2010 13:41, in article Pine.LNX.4.64.1005271422490.30605@medsec1.medien.uni-weimar.de, "stefan-lucks@see-the.signature" wrote: > On Wed, 26 May 2010, (see below) wrote: > >> On 26/05/2010 14:02, in article >> Pine.LNX.4.64.1005261455260.26620@medsec1.medien.uni-weimar.de, >> "stefan-lucks@see-the.signature" wrote: >> >>> I am a university teacher. For me, it makes quite a difference if I either >>> explain students one coherent language where contracts are an integral part >>> of (like Eiffel), or one programming language plus an additional language >>> for the annotations. >>> >> >> Why? > > Because students appreciate coherent concepts. But concepts /= language notations. > More specifically: There is a syntactic gap between SPARK and Ada. I had > given a course on Ada and SPARK recently, and my students seem to be > permanently tempted to focus on the Ada-part, while contracts and proofs > where considered a more "optional" add-on, rather than a necessary and > integral part of their work. Is that an inaccurate perception? SPARK contracts and proofs ARE add-ons. My experience is that CS/SE students always focus on "coding" at the expense of problem analysis, program design, project planning, verification, validation, documentation, and anything else they find less congenial. I doubt that the SPARK notation has much to do with that. > > Beware: My students are some of the people who will > write the software you will use tomorrow. ;-) Since they are learning SPARK/Ada I am less worried by that than I might otherwise have been. 8-) Beware: My ex-students are some of the people who wrote the software you are using today. ;-) -- Bill Findlay chez blueyonder.co.uk