27 Sep
2014
27 Sep
'14
4:09 p.m.
On 27/09/14 5:19 PM, Richard wrote:
In article
<1622761209.431415.1411848409762.JavaMail.root at md02.topaz.synacor.com>,
ANDY HOLT <andy.holt at tesco.net> writes:
However, proving type soundness and other properties is commonly done
today (and is much desired[1]). Much progress has been made in the past
50 years, despite regressive howlers like C.
We _are_ allowed to use a wide range of well-researched mechanical
methods to improve software quality. After all, we have a computer right
here, why waste it.
--Toby
[1] http://qr.ae/cRFJa
Dijkstra's key interest was proving program
correctness (he was a
mathematician). All the stated languages had features that made this
difficult - if not outright impossible.
Proving program correctness was, and remains, a pipe dream.