An Appeal for a Language

I argue that research into software correctness is stunted for
the lack of a crucial tool: a language for describing why
programs are correct (meet some given specification).  Consider:
we have many languages to describe execution, a few languages
to describe specifications, but nothing to explain how a program
interacts with itself to meet that specification.

As a thought experiment, consider trying to argue that a given
pointer dereference in some familiar program will succeed.  That
argument would likely involve a number of high-level concepts
that are difficult to formalize: reachability, lack of sharing,
time since last modification, monotonicity of some set of changes,
etc.

A common, formal language for such arguments, and also appropriate
for comments and annotations, would facilitate correctness research.