Re: GNAT packages in Linux distributions

["(see below)" <yaldnif.w@blueyonder.co.uk>]

On 27/05/2010 13:41, in article
Pine.LNX.4.64.1005271422490.30605@medsec1.medien.uni-weimar.de,
"stefan-lucks@see-the.signature" <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" <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
<surname><forename> chez blueyonder.co.uk