In article <4806C111.6090400 / comcast.net>,
Tom Cloyd  <tomcloyd / comcast.net> wrote:
>My thanks to the core contributors to this fascinating thread. It's 
>stretched me well past my boundaries on several points, but also 
>clarified some key learning I've picked from my own field (psychology & 
>psychotherapy).

Here are a website with some papers that I found in my cursory
research of the topic and might be interesting:

http://www.praxis-his.com/sparkada/publications_journals.asp

The Philosophical Transactions paper by Roderick Chapman reports
that, using SPARK (a well-behaved subset of Ada), "Proof of the
absence of run-time errors has been performed on programs of the
order of 100 000 lines of code."

Francis