From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Sat, 3 Dec 2016 11:23:17 +0100
Date: 2016-12-03T11:23:17+01:00 [thread overview]
Message-ID: <o1u6en$1igc$2@gioia.aioe.org> (raw)
In-Reply-To: o1sj6s$9vp$1@dont-email.me
On 2016-12-02 20:50, G.B. wrote:
> On 02.12.16 17:21, Dmitry A. Kazakov wrote:
>> Predicates are just arbitrary expressions the programmer sets without
>> understanding all effects of his actions.
>
> So are programs.
When written in C?
> While I think I understand the desire for a fully proven
> type centered, consistent, awesome Ada program and supporting
> language, meanwhile a simple
>
> pragma Assert (Is_Sorted (S)); -- S a library level constant
>
> has in effect created a desirable change in behavior of an
> older program here. Even though the behavior so far had not
> caused any concern, a bug was sure lurking.
That is exactly the point. You falsely assume that the effect of
run-time assertion fault would be better than the effect of potential
bug in any given context.
When swapping one bug for another you still have it, and as with all
bugs, the effect is not to predict.
> It's programmers who write programs, improving their understanding
> of a lot of thing that affects their programs, using assertions.
and tracing and tests...
> Now, do assertion distract from learning how to write correct
> programs using types that manage to express them?
Yes they do. It has nothing to do with correct programs, as you change
one bug for another.
> And in such
> a way that an Ada compiler can determine truth at compile time?
This is not how predicates work and has nothing to do with truth. The
only truth about a program is whether it exposes predefined behavior.
The main objection to arbitrary predicates is that they expose an
undefined, undecidable, unexpected, undesired behavior. It is all a
decent software design technique is against.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
next prev parent reply other threads:[~2016-12-03 10:23 UTC|newest]
Thread overview: 195+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-11-28 23:49 Ada 2012 Constraints (WRT an Ada IR) Shark8
2016-11-29 8:17 ` G.B.
2016-11-29 20:32 ` Shark8
2016-11-29 20:44 ` Dmitry A. Kazakov
2016-11-29 20:51 ` Shark8
2016-11-29 21:06 ` Dmitry A. Kazakov
2016-11-29 22:59 ` Shark8
2016-11-30 8:31 ` Dmitry A. Kazakov
2016-11-30 18:28 ` Shark8
2016-11-30 20:26 ` Niklas Holsti
2016-12-01 0:16 ` Shark8
2016-12-01 22:15 ` Randy Brukardt
2016-11-30 20:45 ` Dmitry A. Kazakov
2016-12-01 0:58 ` Shark8
2016-12-01 8:55 ` Dmitry A. Kazakov
2016-12-01 22:26 ` Randy Brukardt
2016-12-02 16:21 ` Dmitry A. Kazakov
2016-12-02 19:15 ` Randy Brukardt
2016-12-03 10:21 ` Dmitry A. Kazakov
2016-12-02 19:50 ` G.B.
2016-12-03 10:23 ` Dmitry A. Kazakov [this message]
2016-12-03 14:02 ` G.B.
2016-12-03 16:26 ` Dmitry A. Kazakov
2016-12-04 15:28 ` Robert Eachus
2016-12-05 8:41 ` Stefan.Lucks
2016-12-05 8:58 ` Dmitry A. Kazakov
2016-12-05 11:09 ` Simon Wright
2016-12-05 18:42 ` Shark8
2016-12-05 22:13 ` Dmitry A. Kazakov
2016-12-06 20:51 ` Shark8
2016-12-06 21:07 ` Dmitry A. Kazakov
2016-12-06 21:44 ` Shark8
2016-12-06 23:23 ` Randy Brukardt
2016-12-07 22:42 ` Shark8
2016-12-07 1:08 ` Dennis Lee Bieber
2016-12-07 6:36 ` Niklas Holsti
2016-12-07 13:10 ` Dennis Lee Bieber
2016-12-07 22:55 ` Brian Drummond
2016-12-08 2:44 ` Shark8
2016-12-07 10:04 ` G.B.
2016-12-07 10:14 ` G.B.
2016-12-07 10:51 ` J-P. Rosen
2016-12-08 18:33 ` G.B.
2016-12-09 8:26 ` J-P. Rosen
2016-12-09 8:56 ` G.B.
2016-12-10 15:13 ` Jacob Sparre Andersen
2016-12-11 19:50 ` Shark8
2016-12-05 22:07 ` Dmitry A. Kazakov
2016-12-06 23:09 ` Randy Brukardt
2016-12-07 10:03 ` Dmitry A. Kazakov
2016-12-07 22:37 ` Randy Brukardt
2016-12-08 8:46 ` Dmitry A. Kazakov
2016-12-10 15:24 ` Jacob Sparre Andersen
2016-12-09 9:12 ` Robert Eachus
2016-12-05 19:22 ` G.B.
2016-12-05 22:18 ` Dmitry A. Kazakov
2016-12-05 22:12 ` Randy Brukardt
2016-12-05 22:26 ` Dmitry A. Kazakov
2016-12-06 9:29 ` Simon Wright
2016-12-06 10:01 ` Dmitry A. Kazakov
2016-12-06 23:15 ` Randy Brukardt
2016-12-07 10:20 ` Dmitry A. Kazakov
2016-12-07 22:26 ` Randy Brukardt
2016-12-08 8:57 ` Dmitry A. Kazakov
2016-12-08 9:42 ` G.B.
2016-12-08 10:03 ` Dmitry A. Kazakov
2016-12-08 18:35 ` G.B.
2016-12-09 9:38 ` Dmitry A. Kazakov
2016-12-11 11:21 ` G.B.
2016-12-11 12:28 ` Dmitry A. Kazakov
2016-12-11 13:31 ` G.B.
2016-12-11 15:40 ` Dmitry A. Kazakov
2016-12-11 20:51 ` G.B.
2016-12-12 8:27 ` Dmitry A. Kazakov
2016-12-12 15:31 ` G.B.
2016-12-12 17:39 ` Dmitry A. Kazakov
2016-12-12 18:55 ` G.B.
2016-12-12 20:53 ` Dmitry A. Kazakov
2016-12-13 7:15 ` G.B.
2016-12-13 8:27 ` Dmitry A. Kazakov
2016-12-13 10:39 ` G.B.
2016-12-13 11:19 ` Dmitry A. Kazakov
2016-12-13 16:59 ` G.B.
2016-12-13 21:11 ` Dmitry A. Kazakov
2016-12-13 22:13 ` Shark8
2016-12-14 8:42 ` Dmitry A. Kazakov
2016-12-14 11:04 ` G.B.
2016-12-14 11:25 ` Dmitry A. Kazakov
2016-12-14 12:44 ` G.B.
2016-12-14 12:52 ` Dmitry A. Kazakov
2016-12-14 16:31 ` G.B.
2016-12-14 16:52 ` Dmitry A. Kazakov
2016-12-14 18:14 ` G.B.
2016-12-14 12:05 ` G.B.
2016-12-14 19:23 ` Shark8
2016-12-14 20:04 ` Dmitry A. Kazakov
2016-12-14 21:46 ` Shark8
2016-12-15 8:41 ` Dmitry A. Kazakov
2016-12-15 10:31 ` G.B.
2016-12-15 13:17 ` Dmitry A. Kazakov
2016-12-15 13:27 ` Dmitry A. Kazakov
2016-12-15 19:50 ` G.B.
2016-12-16 10:04 ` Dmitry A. Kazakov
2016-12-16 11:48 ` G.B.
2016-12-16 12:56 ` Stefan.Lucks
2016-12-16 19:59 ` Randy Brukardt
2016-12-16 20:35 ` G.B.
2016-12-17 9:33 ` Stefan.Lucks
2016-12-19 22:57 ` Randy Brukardt
2016-12-16 13:24 ` Dmitry A. Kazakov
2016-12-15 14:34 ` Shark8
2016-12-15 14:53 ` Dmitry A. Kazakov
2016-12-15 22:34 ` Shark8
2016-12-16 8:28 ` Dmitry A. Kazakov
2016-12-17 3:46 ` Shark8
2016-12-14 12:21 ` G.B.
2016-12-14 12:55 ` Dmitry A. Kazakov
2016-12-14 16:21 ` G.B.
2016-12-14 16:55 ` Dmitry A. Kazakov
2016-12-14 18:55 ` G.B.
2016-12-13 18:25 ` Shark8
2016-12-13 21:11 ` Dmitry A. Kazakov
2016-12-13 22:32 ` Shark8
2016-12-14 8:54 ` Dmitry A. Kazakov
2016-12-14 22:53 ` Randy Brukardt
2016-12-15 8:44 ` Dmitry A. Kazakov
2016-12-15 22:19 ` Randy Brukardt
2016-12-16 8:38 ` Dmitry A. Kazakov
2016-12-16 19:51 ` Randy Brukardt
2016-12-17 9:13 ` Dmitry A. Kazakov
2016-12-19 22:33 ` Randy Brukardt
2016-12-20 11:00 ` Dmitry A. Kazakov
2016-12-21 0:54 ` Shark8
2016-12-21 0:59 ` Randy Brukardt
2016-12-21 15:56 ` Dmitry A. Kazakov
2016-12-21 18:26 ` G.B.
2016-12-21 21:15 ` Dmitry A. Kazakov
2016-12-22 9:54 ` G.B.
2016-12-22 10:16 ` Dmitry A. Kazakov
2016-12-14 11:46 ` G.B.
2016-12-12 19:48 ` Shark8
2016-12-12 20:46 ` Dmitry A. Kazakov
2016-12-12 21:33 ` Shark8
2016-12-13 8:28 ` Dmitry A. Kazakov
2016-12-13 18:53 ` Shark8
2016-12-13 21:11 ` Dmitry A. Kazakov
2016-12-13 22:16 ` Shark8
2016-12-14 9:00 ` Dmitry A. Kazakov
2016-12-11 23:58 ` Paul Rubin
2016-12-12 8:33 ` Dmitry A. Kazakov
2016-12-12 15:23 ` G.B.
2016-12-12 15:51 ` G.B.
2016-12-09 21:46 ` Randy Brukardt
2016-12-13 11:56 ` Alejandro R. Mosteo
2016-12-13 15:02 ` Dmitry A. Kazakov
2016-12-13 17:38 ` Alejandro R. Mosteo
2016-12-05 22:06 ` Randy Brukardt
2016-11-29 17:53 ` Niklas Holsti
2016-11-29 18:21 ` Dmitry A. Kazakov
2016-11-29 20:45 ` Shark8
2016-11-30 0:03 ` Randy Brukardt
2016-11-30 0:59 ` Shark8
2016-12-01 10:33 ` AdaMagica
2016-11-29 23:52 ` Randy Brukardt
2016-11-30 1:24 ` Shark8
2016-11-30 22:12 ` Randy Brukardt
2016-11-30 1:29 ` Shark8
2016-11-30 22:17 ` Randy Brukardt
2016-12-01 1:21 ` Shark8
2016-12-01 22:07 ` Randy Brukardt
2016-12-01 10:06 ` AdaMagica
-- strict thread matches above, loose matches on Subject: below --
2016-12-09 21:41 Randy Brukardt
2016-12-09 22:32 ` Niklas Holsti
2016-12-13 0:41 ` Randy Brukardt
2016-12-13 2:34 ` Shark8
2016-12-13 22:35 ` Randy Brukardt
2016-12-14 0:38 ` Shark8
2016-12-13 20:45 ` Niklas Holsti
2016-12-13 23:19 ` Randy Brukardt
2016-12-14 0:53 ` Shark8
2016-12-14 22:22 ` Randy Brukardt
2016-12-13 22:45 Randy Brukardt
2016-12-14 22:40 Randy Brukardt
2016-12-15 8:48 ` Dmitry A. Kazakov
2016-12-15 22:24 ` Randy Brukardt
2016-12-16 8:40 ` Dmitry A. Kazakov
2016-12-16 19:46 ` Randy Brukardt
2016-12-16 20:14 ` Dmitry A. Kazakov
2016-12-19 22:52 ` Randy Brukardt
2016-12-20 10:59 ` Dmitry A. Kazakov
2016-12-21 0:50 ` Randy Brukardt
2016-12-21 15:56 ` Dmitry A. Kazakov
2016-12-21 22:03 Randy Brukardt
2016-12-21 23:02 ` Shark8
2016-12-21 22:12 Randy Brukardt
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox