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.
