Quotes

"... one could communicate with these machines in any language provided it was an exact language"
"... the system should resemble normal mathematical procedure closely, but at the same time should be as unambiguous as possible."
Alan Turing, 1947
 
"SPARK continues to prove it is the most reliable approach to safety critical software. However, C and its associated forms should be avoided."
from "Software Static Code Analysis Lessons Learned" by Andy German, QinetiQ Boscombe Down. DoD CrossTalk Journal, November 2003. PDF or HTML of this paper is available here.
 
"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 to use."
Professor Tony Hoare, 1980 ACM Turing Award Lecture

"There are two ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies. And the other is to make it so complicated that there are no obvious deficiencies."
Professor Tony Hoare, 1980 ACM Turing Award Lecture
 
"Very few errors have been found in the software during the most rigorous levels of FAA testing, which is being successfully conducted for less than a fifth of the normal cost in industry."
Jim Sutton, on the use of SPARK on the Hercules C130J project,
Lockheed Martin.
 
"Use of SPARK Ada toolset was invaluable in the design, development and safety justification of the SHOLIS software to DEF-STAN 00-55."
Michael Stembridge, Programme Manager (Ultra Electronics)