Re: {Pre,Post}conditions and side effects

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Mon, 11 May 2015 19:28:32 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:146ggcmq4yw40.17j749rax0sqi$.dlg@40tude.net...
>> On Fri, 8 May 2015 18:31:02 -0500, Randy Brukardt wrote:
> ...
>>> *Especially* if you're adding them after the fact -- what would
>>> the point be? The program is already debugged and fielded.
>>
>> Most interesting programs cannot be debugged. It is quite strange, you
>> don't believe correct program exist, but trust "debugged" programs do!
>> (:-))
> 
> Naw, Ada does my debugging. When there's a problem that actually requires 
> debugging, it takes forever for it to get fixed.

That's the problem.

> (Sorry, Tero. ;-) My point 
> as just that a fielded program already has some amount of testing and fixing 
> done to it (we hope), and once that happens, leave it alone until/unless 
> there is a problem.

Either you must have a very high level code quality or you don't care.
Since it is not the latter case, why wouldn't you use C instead? It is the
former. Then we return to the starting point of the discussion. No compiler
and no language, no matter how tedious, can ensure that level upon
compilation. And as you said it is too much burden to require this from
programmers. furthermore, it is simply impossible to achieve in just single
step of developing process. Yet you cannot delay the phase of executable
code forever. Just for pragmatic reasons, most bugs are much simple and
effective to find and eliminate running the code. That is why people buy in
quick-and-dirty approach. Therefore proofs must be optional, their extent
adjustable, the time and place in the developing process up to the
programmer. 

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de