Dicebot on leaving D: It is anarchy driven development in all its glory.

[Timon Gehr]

On 29.08.2018 19:15, H. S. Teoh wrote:
> On Wed, Aug 29, 2018 at 06:58:16PM +0200, Timon Gehr via Digitalmars-d wrote:
>> On 28.08.2018 19:02, H. S. Teoh wrote:
>>> On Tue, Aug 28, 2018 at 08:18:57AM +0000, Eugene Wissner via Digitalmars-d wrote:
>>> [...]
>>>> There are still valid use cases where const should be "broken".
>>>> One of them is mutex (another one caching). I have very little
>>>> experiance in multi-threaded programming, but what do you think
>>>> about "mutable" members, despite the object is const?
>>> The problem with compromising const is that it would invalidate any
>>> guarantees const may have provided.
>>
>> No. You start with the set of allowed program rewrites, then require
>> code with __mutable to not break under them. Code using __mutable is
>> unsafe.
> 
> Currently, immutable implicitly converts to const. If const is allowed
> to be overridden, then you could violate immutable, which is UB.
> ...

__mutable fields are __mutable also in the immutable instance. You might 
get into trouble with shared if you are not careful because of the 
unfortunate "implicit shared" semantics of immutable, but it is up to 
the programmer to get this right.

> 
>>> Const in D is not the same as const in languages like C++; const in
>>> D means*physical*  const, as in, the data might reside in ROM where
>>> it's physically impossible to modify.  Allowing the user to bypass
>>> this means UB if the data exists in ROM.
>>>
>>> Plus, the whole point of const in D is that it is
>>> machine-verifiable, i.e., the compiler checks that the code does not
>>> break const in any way and therefore you are guaranteed (barring
>>> compiler bugs) that the data does not change.  If const were not
>>> machine-verifiable, it would be nothing more than programming by
>>> convention, since it would guarantee nothing.  Allowing const to be
>>> "broken" somewhere would mean it's no longer machine-verifiable (you
>>> need a human to verify whether the semantics are still correct).
>>
>> It is not unusual to need a human to verify that your code does what
>> it was intended to do.
> 
> And it is not unusual for humans to make mistakes and certify code that
> is not actually correct.  Automation provides much stronger guarantees
> than human verification.
> ...

Absolutely. But D only strives to provide such automation in @safe code. 
For @system code, we need a formal specification of what is allowed. 
(And it needs to include all things that the GC and language do; no 
magic.) Note that such a formal specification is a prerequisite for any 
(possibly language-external) automated verification approaches.

> Besides, this is missing the point.  What I meant was that if const
> could be arbitrarily overridden anywhere down the call chain, then the
> compiler could no longer feasibly verify that a particular piece of code
> doesn't violate const. The code could be calling a function for which
> the compiler has no source code, and who knows what that function might
> do. It could override const and modify the data willy-nilly, and if the
> const reference is pointing to an immutable object, you're in UB land.
> 
> Not allowing const to be overridden (without the user deliberately
> treading into UB land by casting it away) allows the compiler to
> statically check that the code doesn't actually modify a const object.
> 
> You appear to be thinking I was making a statement about verifying
> program correctness in general, which is taking what I said out of
> context.
> 
> 
> T
> 

I was thinking you were making a statement about __mutable fields.