Re: XRP

[Craig Carey <research@ijs.co.nz>]

On 29 Apr 2004 00:58:18 -0700, ***@praxis-cs.co.uk (Rod Chapman) wrote:
>Lutz Donnerhacke <lutz@iks-jena.de> 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