Re: about the new Ada 2012 pre/post conditions

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

On Mon, 25 Jun 2012 12:17:14 +0200, Georg Bauhaus wrote:

> On 25.06.12 10:08, Dmitry A. Kazakov wrote:
>> On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote:
>> 
>>> It is a theory in a different universe of notions.
>> 
>> http://en.wikipedia.org/wiki/Paradox_of_the_Court 
> 
> Indeed, it helps to remember that logicians and mathematicians
> have learned that logic and mathematics cannot justify themselves.

No, they never ever did that. From very beginning mathematicians used
axiomatic approach instead. What they did, was constructing frameworks
within which one could not deduce both A and not A.

> We have to do something. DbC is something. Better than nothing.

Is SPARK nothing? Is strong typing nothing?

But you seemingly did not read what I wrote earlier. There is either #1 or
#2. #2 is inconsistent and thus is out. Left is #1: so-called Ada 2012
preconditions simply are misplaced implementations. This is flawed and
misleading, but not because of some cosmogonic problems like your
Promethean trampling laws of logic. Just a much more humble ignoring
principles of good language design. Nothing really new.

> DbC is a best effort thing like every system building effort.

How are you going to prove this, if "DbC" contradicts logic itself?

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