Re: Safety of unprotected concurrent operations on constant objects

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

On Thu, 15 May 2014 11:53:09 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> Because inability to prove that contract X is fulfilled by a party P makes
>> P illegal. [*]
> 
> I know that's your point of view.  I haven't seen you explain why.

Sorry? There are three outcomes of a proof:

1. True
2. False
3. Don't know

And two outcomes of program legality:

A. Legal
B. Illegal

Now map 1,2,3 to A,B. I assume it is:

1 -> A
2 -> B
3 -> B (cannot prove it, assume it is wrong)

You?

> Yeah, I know compile-time checks are good when possible.
> But they're not always possible (as I'm sure you know).
> So insisting on contracts being checked at compile time
> doesn't make my programs better -- it just requires me to
> put "--" before some of my contracts.

?

We were talking about a prover, at least I was. I fail to see how a prover
could be related in any form to run-time. You may say that prover is not
about pseudo-contracts of Ada 2012, I don't care. Use whatever word you
want, but prover is still a compile-time.

>> Unless you accept making illegal programs legal, you must not allow the
>> prover's power to change.
> 
> Every new version of Ada has made some previously-illegal programs
> legal.  An infinite number of them, in fact.  So of course I 
> accept making illegal programs legal.

If you are OK with that, very well. Still you will have to mandate a
well-defined power within each version. Otherwise, legality will depend on
the compiler.

P.S. I thought you were against making

   function Foo return Integer is
   begin
      raise Constraint_Error;
   end Foo;

legal?

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