DIP 1009--Improve Contract Usability--Preliminary Review Round 1

[Moritz Maxeiner via Digitalmars-d]

On Saturday, 24 June 2017 at 05:16:45 UTC, MysticZach wrote:
> On Friday, 23 June 2017 at 21:36:07 UTC, Moritz Maxeiner wrote:
>> Contracts within the DbC paradigm *are* abstractions that do 
>> not necessitate any particular implementation.
>
> In practice, though, what must any such implementation actually 
> achieve?
> [...]
> 2. prevent programs in invalid states from continuing

With "program" in this abtract domain meaning the specific 
computational task that broke the contract, not necessarily the 
entire implementation domain OS process - it's just that the 
finest safe termination of computational tasks in the presence of 
bugs on modern OSs you get for free (because of process 
isolation) is a process.
With a runtime environment (e.g. a VM like the JVM, or an 
appropriate druntime implementation) that supports safe killing 
on a finer resolution (e.g. threads and fibers) there's no 
inherent reason not to map contract violations to thread/fiber 
killing instead of process killing (if it's proven to be safe 
within that runtime).

> 3. provide information about those invalid states after the fact

All it *must* do is identify which contract failed (i.e. 
(file,line/row,column)). The rest is optional.

>> It would only couple the contracts with asserts if the DIP 
>> also specifies that asserts *must* be used for the lowering 
>> (which I would be against btw).
>
> [...]. I'd rather not deal with that problem. It's vastly 
> easier to just put my faith into the `assert` grammar, and hope 
> that any improvements that it needs and receives will apply 
> equally to `assert`s as well.

I would simply copy the current assert grammar into a separate 
contract grammar, so that further modifications to the assert 
grammar do not change the new contract grammar.
But as I said, it's not important to me, it was just an 
observation/question. Should the need ever arise for (new) 
contract and assert grammar to diverge it can be dealt with then 
by whoever does the diverging.