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.1 required=5.0 tests=BAYES_00,
	PP_MIME_FAKE_ASCII_TEXT autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,39579ad87542da0e
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
X-Received: by 10.180.20.105 with SMTP id m9mr1648856wie.5.1368583765068;
        Tue, 14 May 2013 19:09:25 -0700 (PDT)
MIME-Version: 1.0
Path: 
 hg5ni110158wib.1!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.cambriumusenet.nl!feed.tweaknews.nl!194.109.133.81.MISMATCH!newsfeed.xs4all.nl!newsfeed2.news.xs4all.nl!xs4all!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!News.Dal.Ca!news.litech.org!news.etla.org!feeder.erje.net!eu.feeder.erje.net!nuzba.szn.dk!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Seeking for papers about tagged types vs access to subprograms
Date: Fri, 10 May 2013 19:18:30 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <kmk2on$tij$1@loke.gir.dk>
References: <op.wv8jh1c1ule2fv@cardamome> <op.wwnp2zkrule2fv@cardamome>
 <u3jaslg5kca7.1gk5ds3d4sx2y$.dlg@40tude.net> <op.wwnsmtteule2fv@cardamome>
 <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <op.wwny5jerule2fv@cardamome>
 <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> <op.wwn4oak8ule2fv@cardamome>
 <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <kmbohm$elb$1@loke.gir.dk>
 <p0pf97g5w6xg.jhca6ztjwpde$.dlg@40tude.net> <op.wwq9s4l6ule2fv@cardamome>
 <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> <op.wwrefx1pule2fv@cardamome>
 <cps71yzogw24$.7ol98fxcaurj$.dlg@40tude.net> <op.wwriky0dule2fv@cardamome>
 <nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net> <kmecg6$et4$1@loke.gir.dk>
 <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> <kmh7d4$up3$1@loke.gir.dk>
 <op.wwumn3r2ule2fv@cardamome> <av4r5qFitfiU1@mid.individual.net>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: loke.gir.dk 1368231511 30291 69.95.181.76 (11 May 2013 00:18:31 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Sat, 11 May 2013 00:18:31 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Date: 2013-05-10T19:18:30-05:00
List-Id: <comp.lang.ada>

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:av4r5qFitfiU1@mid.individual.net...
> On 13-05-10 06:29 , Yannick Duch�ne (Hibou57) wrote:
>> Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt
> ...
>>> Yes, because we need to move beyond typing to other forms of static 
>>> error
>>> detection. Typing is too rigid to do a good job -- you need to include
>>> statically known information about the contents of variables and
>>> parameters,
>>> which can change from line-to-line in a program.
>>
>> I feel the same. I often though typing can't do everything if it comes
>> with value type checking, while in some occasions, I tried to express
>> each validity condition with types and then type checking (that ends to
>> be crazy, indeed). A simple example, is paired invocation, where
>> whenever a sub-program is is invoked, sooner or later, another
>> sub-program must be invoked too on the same argument, ex. like `Open`
>> and later `Close`. This cannot be expressed with types and indeed
>> requires assertions.
>
> Are you familiar with the "typestate" concept? As I understand it, the
> intent is to check state-sequence rules such as Open-followed-by-Close.
> See http://en.wikipedia.org/wiki/Typestate_analysis.

Thanks for the reference. I doubted that the idea was new (there are no new 
ideas), but I hadn't heard of it before. I don't like the name much, because 
it feeds into the "type is everything" madness that Dmitry exhibits so 
clearly. This clearly (just like constraints and predicates) is something 
that's added in addition to type analysis; it's not part of it at all.

                                      Randy.