On Wednesday, 30 July 2014 at 14:36:30 UTC, Ary Borenszweig wrote:
Could you show an example that's a bit more complex and useful?
I'm with Walter that I don't see any difference between assert
and assume.
assume provide additional axioms to the ones implicit in the
program.
assert provide theorems to be proven.
assume provide claims that already are proven (or just defined as
a requirement imposed on the environment).
For instance after a system call, you might have a specification
that states exactly what you can assume after it returns. That
specification you can specify as assume() and you can optimize on
those, safely.
assert() you cannot optimize on safely. Those are theorems that
are yet to be proven.
