From: Peter Amey <pna@erlang.praxis-cs.co.uk>
Subject: Re: Any research putting c above ada?
Date: 1997/04/16
Date: 1997-04-16T00:00:00+00:00 [thread overview]
Message-ID: <Pine.SUN.3.91.970416082842.5291A-100000@erlang.praxis-cs.co.uk> (raw)
In-Reply-To: 5j078b$b25$1@NNTP.MsState.Edu
On 15 Apr 1997, Tom White wrote:
> I remember a Turing Award Lecture by C.A.R. Hoare from the early
> eighties (dig through some Journals of the ACM). Hoare was not
> an Ada booster; he was concerned about the complexity of Ada from
> both the application programmer's and compiler implementor's
> perspectives.
>
> As to your second point, Hoare was accepting the award :)
>
> --
> -- Tom White <tom@net.msstate.edu>
>
A quote from this 1980 lecture includes the following:
"It is not too late! I believe that by careful pruning of the Ada
language, it is still possible to select a very powerful subset that would
be reliable and efficient in implementation and safe and economic in use".
This was part of the inspiration for SPARK, our formally-defined,
tool-supported, secure SPARK subset.
There is another important point here as well: the difference between Ada
and most other languages is not just the detail of whether incompatible
types can be coerced or whether run-time checks are turned on or off by
default. Rather it is that Ada makes a serious attempt to define the
semantics of the language under all conditions including those where
errors have occurred. This gives the desirable (essential?) property that
the meaning of a program can be determined by looking at the source code
(especially if it is SPARK) rather than by reviewing the test results :-)
This property of Ada is what makes secure subsets feasible (and the nice
things that follow from this - like being able to construct a proof, prior
to execution, that a SPARK program is exception free). It would not be
possible to define a subset of C that had all SPARK's properties because
after cutting away the ambiguity and insecurity what would be left would
be too small to be useful.
Peter
next prev parent reply other threads:[~1997-04-16 0:00 UTC|newest]
Thread overview: 295+ messages / expand[flat|nested] mbox.gz Atom feed top
1997-04-09 0:00 Any research putting c above ada? Konstantin B. Goldin
1997-04-10 0:00 ` Richard Krehbiel
1997-04-10 0:00 ` Tom Wheeley
1997-04-11 0:00 ` Richard Kenner
1997-04-16 0:00 ` Daniel P Hudson
1997-04-17 0:00 ` Stephen Leake
1997-04-10 0:00 ` Philip Brashear
1997-04-10 0:00 ` CubanPete
1997-04-11 0:00 ` John Thomas Apa
1997-04-10 0:00 ` Andrew Dunstan
1997-04-11 0:00 ` Gary W Smith
1997-04-11 0:00 ` James Youngman
1997-04-11 0:00 ` Steve Summit
1997-04-12 0:00 ` Dave Wood
1997-04-14 0:00 ` Chris Lomont
1997-04-16 0:00 ` Dave Wood
1997-04-11 0:00 ` Steve Jones - JON
1997-04-11 0:00 ` Kaz Kylheku
1997-04-12 0:00 ` Tom Wheeley
[not found] ` <01bc46be$fb54cae0$3f6700cf@default>
1997-04-13 0:00 ` Kaz Kylheku
1997-04-14 0:00 ` Craig Franck
[not found] ` <33526cbf.41c6@cca.rockwell.com>
[not found] ` <5iusvd$118e@newssvr01-int.news.prodigy.com>
1997-04-14 0:00 ` James S. Rogers
[not found] ` <3353a187.1062@bix.com>
1997-04-16 0:00 ` Matthew Givens
1997-04-17 0:00 ` Tom Moran
[not found] ` <33545F8D.2AF4@worldnet.att.net>
[not found] ` <335569F1.55A0@pratique.fr>
1997-04-20 0:00 ` Nick Roberts
[not found] ` <33541be1.14961570@news.airmail.net>
1997-04-16 0:00 ` Matthew Givens
1997-04-16 0:00 ` Dale Stanbrough
[not found] ` <33530e22.5940@worldnet.att.net>
1997-04-16 0:00 ` Matthew Givens
1997-04-18 0:00 ` Kenneth Almquist
1997-04-20 0:00 ` Matthew Givens
1997-04-22 0:00 ` Alan Brain
[not found] ` <335d880c.324@dynamite.com.au>
1997-05-04 0:00 ` Matthew Givens
1997-05-05 0:00 ` Alan Brain
[not found] ` <336ea9ca.3c92@dynamite.com.au>
1997-05-07 0:00 ` Matthew Givens
1997-05-06 0:00 ` Tom Moran
1997-05-07 0:00 ` Jon S Anthony
1997-05-07 0:00 ` Jon S Anthony
1997-05-07 0:00 ` Kevin Cline
[not found] ` <5aedd9b0882ea1bf.69856d7f77cd2ae3.229bf1374681c88b@library-proxy.airnews.net>
1997-05-10 0:00 ` Matthew Givens
1997-05-10 0:00 ` Robert S. White
1997-05-11 0:00 ` Kevin Cline
1997-05-16 0:00 ` brad.balfour
1997-05-14 0:00 ` T Wheeley
1997-04-19 0:00 ` Tom Wheeley
[not found] ` <5j0e5i$qgi@bcrkh13.bnr.ca>
1997-04-16 0:00 ` Matthew Givens
[not found] ` <5j4ijn$3ta1@news.knox.edu>
1997-04-17 0:00 ` Kaz Kylheku
1997-04-18 0:00 ` Tim Behrendsen
[not found] ` <33552C53.41C6@cca.rockwell.com>
1997-04-20 0:00 ` Steve Doiel
1997-04-20 0:00 ` Jay Martin
1997-04-21 0:00 ` Robert I. Eachus
1997-04-14 0:00 ` Roy Grimm
1997-04-11 0:00 ` Terry Colligan
1997-04-11 0:00 ` Larry J. Elmore
1997-04-12 0:00 ` Terry Colligan
[not found] ` <3359e813.340466234@news.pacificnet.net>
1997-04-11 0:00 ` James S. Rogers
1997-04-12 0:00 ` Danette & Murray Root
1997-04-12 0:00 ` Steve Summit
1997-04-12 0:00 ` Dave Wood
[not found] ` <3373409f.494266577@news.pacificnet.net>
1997-04-13 0:00 ` Dave Wood
[not found] ` <E8pxJ0.I3s@thomsoft.com>
[not found] ` <3355E0F2.56E5@aonix.com>
1997-04-18 0:00 ` David Hanley
1997-04-20 0:00 ` Nick Roberts
1997-04-14 0:00 ` Robert S. White
1997-04-14 0:00 ` Kaz Kylheku
1997-04-15 0:00 ` Robert S. White
[not found] ` <5ivtcu$puv@huron.eel.ufl.edu>
1997-04-16 0:00 ` Kaz Kylheku
1997-04-16 0:00 ` Byron
1997-04-16 0:00 ` John Winters
[not found] ` <5j31dt$o3j@huron.eel.ufl.edu>
1997-04-17 0:00 ` Kaz Kylheku
1997-04-18 0:00 ` David Thornley
[not found] ` <338a1835.439086993@news.pacificnet.net>
1997-04-25 0:00 ` Alan Bowler
[not found] ` <01bc4da9$75237100$f4f582c1@xhv46.dial.pipex.com>
1997-04-21 0:00 ` Daniel P Hudson
1997-04-21 0:00 ` Robert I. Eachus
1997-04-14 0:00 ` Kaz Kylheku
1997-04-14 0:00 ` Stephen Leake
1997-04-13 0:00 ` Larry Kilgallen
1997-04-12 0:00 ` David Weller
1997-04-13 0:00 ` Kaz Kylheku
1997-04-27 0:00 ` Richard Riehle
1997-04-29 0:00 ` Kaz Kylheku
1997-04-30 0:00 ` Roy Grimm
1997-04-30 0:00 ` Kaz Kylheku
1997-04-30 0:00 ` Jay Martin
1997-05-02 0:00 ` Samuel A. Mize
1997-05-05 0:00 ` Roy Grimm
1997-05-06 0:00 ` Robert I. Eachus
1997-05-07 0:00 ` Jay Martin
1997-05-07 0:00 ` Kaz Kylheku
1997-05-08 0:00 ` Jay Martin
1997-05-08 0:00 ` Kevin Cline
1997-05-09 0:00 ` Alan Brain
1997-05-08 0:00 ` Robert I. Eachus
1997-05-09 0:00 ` Kevin Cline
1997-05-11 0:00 ` deafen
1997-05-12 0:00 ` Kaz Kylheku
1997-05-12 0:00 ` Roy Grimm
1997-05-01 0:00 ` Roy Grimm
1997-05-01 0:00 ` Jay Martin
1997-05-01 0:00 ` Kaz Kylheku
1997-05-02 0:00 ` Roy Grimm
1997-05-02 0:00 ` Jon S Anthony
1997-05-05 0:00 ` Steve Furlong
1997-05-06 0:00 ` Robert A Duff
1997-05-06 0:00 ` Kevin Cline
1997-05-06 0:00 ` Jon S Anthony
1997-05-08 0:00 ` Lawrence Kirby
1997-05-14 0:00 ` T Wheeley
1997-05-14 0:00 ` Kaz Kylheku
1997-05-10 0:00 ` Fritz W Feuerbacher
1997-05-11 0:00 ` Wilbur Streett
1997-05-12 0:00 ` Kevin Cline
1997-05-20 0:00 ` T Wheeley
1997-04-30 0:00 ` Robert I. Eachus
1997-04-30 0:00 ` Kaz Kylheku
1997-05-01 0:00 ` Robert I. Eachus
1997-05-03 0:00 ` Student responsability (Was: Any research putting c above ada?) Laurent Gasser
1997-05-03 0:00 ` John Bode
1997-05-05 0:00 ` Steven Huang
1997-05-05 0:00 ` Any research putting c above ada? John Apa
1997-05-06 0:00 ` Kevin Cline
1997-05-06 0:00 ` Roy Grimm
1997-05-07 0:00 ` Kevin Cline
1997-05-07 0:00 ` Roy Grimm
1997-05-07 0:00 ` Kaz Kylheku
1997-05-08 0:00 ` Kevin Cline
1997-05-08 0:00 ` Roy Grimm
1997-05-08 0:00 ` Kaz Kylheku
1997-05-09 0:00 ` Kevin Cline
1997-05-10 0:00 ` Dan Shea
1997-05-11 0:00 ` Kevin Cline
1997-05-07 0:00 ` John Apa
1997-05-08 0:00 ` Roy Grimm
1997-05-08 0:00 ` Kevin Cline
1997-05-10 0:00 ` John Apa
1997-05-11 0:00 ` Kevin Cline
1997-05-14 0:00 ` Nick Roberts
1997-05-08 0:00 ` Alan Brain
1997-05-07 0:00 ` Adam Beneschan
1997-05-09 0:00 ` Richard A. O'Keefe
1997-05-09 0:00 ` Larry Weiss
1997-05-11 0:00 ` Kevin Cline
1997-05-11 0:00 ` Jay Martin
1997-05-12 0:00 ` Kevin Cline
1997-05-12 0:00 ` Robert I. Eachus
1997-05-14 0:00 ` Kevin Cline
1997-05-12 0:00 ` Craig Franck
1997-05-12 0:00 ` Kevin Cline
1997-05-13 0:00 ` Craig Franck
1997-05-13 0:00 ` Jonathan Guthrie
1997-05-14 0:00 ` Mathew Hendry
[not found] ` <F4243E31257E3230.1400B453F19F7D1B.A88AC4B6A31D <5l8gf8$2jp@mtinsc05.worldnet.att.net>
1997-05-13 0:00 ` Kaz Kylheku
1997-05-13 0:00 ` Lawrence Kirby
1997-05-14 0:00 ` T Wheeley
1997-05-15 0:00 ` Ray Blaak
1997-05-16 0:00 ` Alan Brain
[not found] ` <5lb2mi$3i2@mtinsc03.worldnet.att.net>
1997-05-14 0:00 ` Jonathan Guthrie
1997-05-14 0:00 ` Szu-Wen Huang
1997-05-15 0:00 ` Jonathan Guthrie
[not found] ` <EA8sny.HKJ@thinkage.on.ca>
1997-05-16 0:00 ` W. Wesley Groleau (Wes)
[not found] ` <rayEA5A7D.932@netcom.com>
1997-05-14 0:00 ` Steve Jones - JON
1997-05-14 0:00 ` W. Wesley Groleau (Wes)
1997-05-17 0:00 ` Robert I. Eachus
1997-05-14 0:00 ` M. Prasad
1997-04-30 0:00 ` Jay Martin
1997-05-01 0:00 ` Robert I. Eachus
1997-05-05 0:00 ` Jay Martin
1997-05-06 0:00 ` Kevin Cline
1997-05-07 0:00 ` Robert I. Eachus
1997-05-01 0:00 ` Kevin Cline
1997-04-30 0:00 ` Jon S Anthony
1997-05-01 0:00 ` Kaz Kylheku
1997-05-02 0:00 ` Jon S Anthony
1997-05-03 0:00 ` Craig Franck
1997-05-03 0:00 ` Matthew Givens
1997-05-03 0:00 ` Robert S. White
[not found] ` <33508283.56dd@aonix.com>
[not found] ` <33526280.62b3@gsfc.nasa.gov>
[not found] ` <5ivths$pv2@huron.eel.ufl.edu>
1997-04-16 0:00 ` Matthew Givens
[not found] ` <m2ragbrmij.fsf@acm.org>
1997-04-20 0:00 ` Nick Roberts
1997-04-14 0:00 ` Alan Brain
1997-04-17 0:00 ` Jon S Anthony
1997-04-10 0:00 ` Daniel P Hudson
1997-04-10 0:00 ` Thomas Aho
1997-04-10 0:00 ` Bob Stout
1997-04-10 0:00 ` Matthew Heaney
1997-04-14 0:00 ` Steve Jones - JON
1997-04-14 0:00 ` Kaz Kylheku
1997-04-15 0:00 ` Matthew Givens
1997-04-20 0:00 ` Alan Brain
[not found] ` <335ae79e.55ed@dynamite.com.au>
1997-04-20 0:00 ` Matthew Givens
1997-04-28 0:00 ` Andrew Dunstan
1997-04-29 0:00 ` Matthew Givens
1997-05-06 0:00 ` Andrew Dunstan
1997-05-07 0:00 ` Kevin Cline
1997-05-07 0:00 ` Jon S Anthony
1997-05-07 0:00 ` Jeff Carter
1997-05-08 0:00 ` Robert I. Eachus
1997-05-09 0:00 ` Kevin Cline
1997-05-09 0:00 ` John G. Volan
1997-05-11 0:00 ` Kevin Cline
1997-05-12 0:00 ` John G. Volan
1997-05-12 0:00 ` John G. Volan
1997-05-13 0:00 ` Alan Brain
1997-05-14 0:00 ` Kevin Cline
1997-05-16 0:00 ` Alan Brain
1997-05-17 0:00 ` Kevin Cline
1997-05-17 0:00 ` John G. Volan
1997-05-18 0:00 ` Kevin Cline
1997-05-18 0:00 ` Jon S Anthony
1997-05-18 0:00 ` Brian Rogoff
1997-05-19 0:00 ` Kevin Cline
1997-05-19 0:00 ` Jon S Anthony
1997-05-19 0:00 ` John G. Volan
1997-05-20 0:00 ` Kevin Cline
1997-05-20 0:00 ` Jeff Carter
1997-05-21 0:00 ` Brian Rogoff
1997-05-21 0:00 ` STL in Ada95 [was: Any research putting c above ada?] John G. Volan
1997-05-22 0:00 ` Brian Rogoff
1997-05-23 0:00 ` Jon S Anthony
1997-05-24 0:00 ` Brian Rogoff
1997-05-22 0:00 ` Brian Rogoff
1997-05-23 0:00 ` Iterator Syntax [was: Re: STL in Ada95] Jeff Carter
1997-05-23 0:00 ` Michel Gauthier
1997-05-23 0:00 ` John G. Volan
1997-05-23 0:00 ` Brian Rogoff
1997-05-21 0:00 ` Any research putting c above ada? Alan Brain
1997-05-17 0:00 ` Dale Stanbrough
1997-05-12 0:00 ` Robert I. Eachus
1997-04-30 0:00 ` Daniel P Hudson
1997-04-30 0:00 ` Adam Beneschan
1997-05-02 0:00 ` Daniel P Hudson
[not found] ` <5j078b$b25$1@NNTP.MsState.Edu>
1997-04-16 0:00 ` Peter Amey [this message]
[not found] ` <5j31lj$qnk@huron.eel.ufl.edu>
1997-04-24 0:00 ` Suzette Norby
1997-04-25 0:00 ` Kaz Kylheku
1997-04-26 0:00 ` Mike Haertel
1997-04-26 0:00 ` Kaz Kylheku
1997-04-27 0:00 ` Nick Roberts
1997-04-28 0:00 ` Istvan.Simon
1997-04-26 0:00 ` Larry Wissig
1997-04-26 0:00 ` Kaz Kylheku
1997-04-26 0:00 ` Nick Roberts
1997-04-26 0:00 ` Lawrence Kirby
1997-04-27 0:00 ` b-see
1997-04-28 0:00 ` Jon S Anthony
1997-04-27 0:00 ` Jerry van Dijk
1997-04-25 0:00 ` Craig Franck
1997-04-28 0:00 ` Jon S Anthony
1997-04-29 0:00 ` Andrew Koenig
1997-04-29 0:00 ` Tom Moran
1997-04-30 0:00 ` Kaz Kylheku
1997-04-30 0:00 ` Robert I. Eachus
1997-05-01 0:00 ` Alan Brain
1997-04-30 0:00 ` Jon S Anthony
1997-05-01 0:00 ` Kaz Kylheku
1997-04-30 0:00 ` Craig Franck
1997-04-30 0:00 ` Robert I. Eachus
1997-04-30 0:00 ` Pat Rogers
1997-05-02 0:00 ` Jon S Anthony
1997-05-01 0:00 ` Jon S Anthony
1997-04-17 0:00 ` Daniel P Hudson
[not found] ` <335458A4.4C1D@worldnet.att.net>
[not found] ` <5j416b$hau@mtinsc04.worldnet.att.net>
1997-04-18 0:00 ` Mark & Zurima McKinney
1997-04-19 0:00 ` Craig Franck
1997-04-21 0:00 ` Robert I. Eachus
[not found] ` <5j30oa$ia9@bcrkh13.bnr.ca>
[not found] ` <3355739E.7B24@pratique.fr>
1997-04-18 0:00 ` Kaz Kylheku
1997-04-23 0:00 ` David Emery
1997-04-17 0:00 ` Jon S Anthony
1997-04-17 0:00 ` Chris Morgan
1997-04-17 0:00 ` Jon S Anthony
1997-04-18 0:00 ` David Emery
1997-04-21 0:00 ` Jim Hyslop
-- strict thread matches above, loose matches on Subject: below --
1997-04-10 0:00 tmoran
1997-04-11 0:00 ` Richard Krehbiel
1997-04-17 0:00 Marin David Condic, 561.796.8997, M/S 731-93
1997-05-03 0:00 tmoran
1997-05-03 0:00 ` Jon S Anthony
1997-05-15 0:00 Jon S Anthony
1997-05-15 0:00 ` Kaz Kylheku
1997-05-15 0:00 ` Jon S Anthony
[not found] ` <01bc6189$b074f500$LocalHost@xhv46.dial.pipex.com>
1997-05-16 0:00 ` Kaz Kylheku
1997-05-16 0:00 ` Jon S Anthony
1997-05-18 0:00 ` Nick Roberts
1997-05-19 0:00 ` Michael Norrish
1997-05-20 0:00 ` Jon S Anthony
1997-05-20 0:00 ` Kaz Kylheku
1997-05-20 0:00 ` Jon S Anthony
1997-05-20 0:00 ` Michael Norrish
1997-05-20 0:00 ` Jon S Anthony
1997-05-20 0:00 ` Kaz Kylheku
1997-05-20 0:00 ` Jon S Anthony
1997-05-21 0:00 ` Kaz Kylheku
1997-05-21 0:00 ` Craig Franck
1997-05-20 0:00 ` Les Hazlewood
1997-05-20 0:00 ` Jason A Cunningham
1997-05-21 0:00 ` Stephan Wilms
1997-05-21 0:00 ` Jason A Cunningham
1997-05-16 0:00 ` T Wheeley
1997-05-16 0:00 ` Jon S Anthony
1997-05-16 0:00 Jon S Anthony
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox