[SystemSafety] systemsafety Digest, Vol 54, Issue 14

[Roderick Chapman]

On the topic of the use of the word "safe" with respect to programming 
languages...
For what it's worth... our experience:

1. About 15 years ago, we (meaning the SPARK R&D team, my colleagues and
predecessors at Altran, Praxis and PVL) decided that we would never
describe SPARK as a "safe language" or a "safe subset" since it gave the
wrong impression, and was open to such obvious mis-interpretation.

2. We have described SPARK as a "language that's appropriate for 
high-integrity
applications" or similar.

3. Programming language people do use the terms "type-safe" and
"memory-safe" with reasonably precise meaning, although even those
concepts are rather language and context-dependent. For example, a 
language might
be _dynamically_ type safe through requiring the use of typing checks
that are executed at runtime and fall back on some sort of exception 
handling
mechanism if they fail.  In Ada, for example, checking of numeric ranges,
overflows, division-by-zero and memory exhaustion are all dynamically 
checked
and raise an exception on failure.

4. This is _very_ different from "static type safety" where _all_ the 
type checking
is done pre-compilation by a theorem prover, abstract interpretation, or 
similar
technologies. SPARK falls into this category.

5. Note that (most annoyingly) SPARK /= Apache SPARK /= SPARC (tm). I now
have to find myself explaining that all the time since Apache SPARK came 
along... :-(

  - Rod