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-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,ddb34e4ee5e28db0 X-Google-Attributes: gid103376,public Path: controlnews3.google.com!news1.google.com!news.glorb.com!newsfeed.berkeley.edu!ucberkeley!enews.sgi.com!news.xtra.co.nz!53ab2750!not-for-mail From: Craig Carey Newsgroups: comp.lang.ada Subject: Re: XRP Message-ID: References: <20040425224751.C907A4C4136@lovelace.ada-france.org> X-Newsreader: Forte Free Agent 2.0/32.652 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Date: Mon, 03 May 2004 13:42:27 +1200 NNTP-Posting-Host: 210.54.66.94 X-Complaints-To: newsadmin@xtra.co.nz X-Trace: news.xtra.co.nz 1083548544 210.54.66.94 (Mon, 03 May 2004 13:42:24 NZST) NNTP-Posting-Date: Mon, 03 May 2004 13:42:24 NZST Organization: Xtra Xref: controlnews3.google.com comp.lang.ada:190 Date: 2004-05-03T13:42:27+12:00 List-Id: On 29 Apr 2004 00:58:18 -0700, ***@praxis-cs.co.uk (Rod Chapman) wrote: >Lutz Donnerhacke wrote: ... >If you're really serious about a high-integrity implementation, >then why not do it in SPARK? We'd might be able to support >such an effort (in terms of tools and support, if not actual >engineering effort... :-) ) > >The SPARK toolset is, of course, totally free to University faculty... > - Rod, SPARK Team Indeed, SparkAda's availability seems to drop a lot if a vice-chancellor expells a computer science professor, etc.. University faculties: http://www.praxis-cs.co.uk/sparkada/universities.asp Suppose hypothetically that an Australian computer science professor was forced out of the university. E.g. there is the case of Mr Ted Steele of Wollongong University, who was dismissed on 26 Feb 2001 (by vice-chancellor, Mr G. Sutton): http://www.nteu.org.au/campaigns/archive/steele/3751/3752 "Timeline" http://www.nteu.org.au/gui/search/index.php?searchQuery=steele and eventually "re-instated by the University in April 2002": http://www.nteu.org.au/news/2002/2002/4283 If the associate professor and molecular immunologist had of been in the topic of computer science, and the only enthusiast for Praxis's software, then they could have missed out in that interval. http://www.uow.edu.au/science/biol/hon_assess/Steele%20Trap.pdf "Steel Trap" "[Mr Steele had] dissented from the averaged marks given by one external and two internal examiners to a local HECS honours student he had supervised." Spark has an impressive list of restrictions. I didn't see error messages produced by the software (a listing of proof syntax errors and warnings). It seemed that generic packages can't contain only type declarations. What is the species of the bird in the PDFs?. Craig Carey