"Strong typing vs. strong testing"

[guthrie]

An interesting archive article on the topic of correctness, and the
layers thereof:

   Program verification: the very idea;
   Communications of the ACM
   Volume 31 ,  Issue 9  (September 1988)
   Pages: 1048 - 1063
   Year of Publication: 1988
   ISSN:0001-0782
"The notion of program verification appears to trade upon an
equivocation. Algorithms, as logical structures, are appropriate
subjects for deductive verification. Programs, as causal models of
those structures, are not. The success of program verification as a
generally applicable and completely reliable method for guaranteeing
program performance is not even a theoretical possibility."

And:
   The proof of correctness wars;
    Communications of the ACM  archive
    Volume 45 ,  Issue 8  (August 2002)
    COLUMN: Practical programmer Pages: 19 - 21
    Year of Publication: 2002
    ISSN:0001-0782
"Whether mild or raging, wars about topics ranging from programming
languages to methods of indentation are healthy for our field"

One central point in the discussions is that the correctness of a
(running) program is different than just that of a piece of code - it
also depends on the compiler, OS, and underlying hardware layers.