On Monday, 11 November 2019 at 22:30:18 UTC, Timon Gehr wrote:
> On 11.11.19 11:39, Walter Bright wrote:
>> 
>> The distinction between assert and assume has come up before, and I've argued that in D they are the same.
>
> Which I have argued is complete insanity. I'm getting pretty angry here. Not sure what to do about it.

I'd expect a FV DIP to hash this out and get everybody on the same page. Different languages, different textbooks, different mathematicians all use slightly different vocabularies for this stuff, so it can get confusing.

Other languages are pretty clear on the distinction between assumptions and assertions. F* ("assume" - https://www.riseforfun.com/FStar/tutorialcontent/guide#h24) & SPARK ("pragma Assume" - https://docs.adacore.com/spark2014-docs/html/ug/en/source/assertion_pragmas.html) both make clear that assumptions are treated like axioms in their provers, and must be used with caution. The Boogie IVL ("assume" - http://chrisposkitt.com/files/teaching/SV-2015-AutoActiveVerification.pdf) works the same way.

Coq has no "assume" keyword, but the "assumption" tactic takes a hypothesis/premise and if it matches the goal (thing you're trying to prove/assert), then it solves the goal).

Frama-C/ANSI C Specification Language ("assumes" clause - https://frama-c.com/download/acsl-1.14.pdf) just treats assumptions as hypotheses/premises that imply some conclusion, so pre-conditions, as far as I can tell. This might be where Walter is coming from in saying that Asserts and Assumes would be the same in D. This is the only example I could find that uses "assume" like this, but there may be others.

I think _most_ people consider Assert vs Assume the way SPARK and F* do - as seen here: https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/

But hey, as Frama-C shows, it's not the only way to interpret those keywords. The English language gets in our way sometimes. Inflammable = flammable, and all that.

If "assume" is taken to mean an "assert" which is a pre-condition, then fine, we could always point to Frama-C/ACSL to show that D isn't some insane outlier and that we aren't a bunch of backwards idiots. It wouldn't be the way _I_ would do it, but that's just one man's opinion, and I'm biased by my use of SPARK where pragma Assume has a clear meaning and works fine.

Given that we already have assert() in in{} contracts, to me the assume() keyword (in Walter's reckoning of the meaning) is redundant, and could be used for the axiomatic meaning.

If in{} and out{} contracts ever disappeared from the language, I think an external solver would need something like assume()/require() to distinguish preconditions from normal assertions.

Having said all that, we probably need to use a little more mathematical rigor with how we define these regardless of the words we choose to describe the concepts.

It would also mean we'd need another keyword/UDA to use for an axiom, like, uh, @axiom. But then we're getting into weird math terms that scare people off. So that's probably why "assume" is preferred by some of the others.

-Doc

On Tuesday, 12 November 2019 at 04:25:57 UTC, Doc Andrew wrote:
> so pre-conditions, as far as I can tell. This might be where Walter is coming from in saying that Asserts and Assumes would be the same in D. This is the only example I could find that uses "assume" like this, but there may be others.

He meant that asserts are turned into assumes as an optimization. He has explained his position before in an older thread. It kinda might work in some settings if you can limit the assumed facts to a single function, but that is not how LLVM works. So it could work in dmd, but a bit dangerous. It would be a disaster in the two other D compilers.

Microsoft c++ uses __assume for giving facts to the optimizer. D should stick with that,

On 11/11/2019 8:25 PM, Doc Andrew wrote:
> I think _most_ people consider Assert vs Assume the way SPARK and F* do - as seen here: https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/ 

Which says:

"Intuitively, Assert is something that you expect the static checker be able to prove at compile time, whereas Assume is something that the static checker can rely upon, but it will not try to prove. At runtime Assert and Assume behave the same: If the condition is false, then the program fails – how it fails (e.g., throwing an exception, opening a dialog box, etc. can be completely customized with CodeContracts)."

Therefore after the Assert, the prover can assume the Assert condition is true. If the prover can prove the Assert is always true, the runtime check can be safely removed.

On 12.11.19 10:12, Walter Bright wrote:
> On 11/11/2019 8:25 PM, Doc Andrew wrote:
>> I think _most_ people consider Assert vs Assume the way SPARK and F* do - as seen here: https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/ 
> 
> 
> Which says:
> 
> "Intuitively, Assert is something that you expect the static checker be able to prove at compile time, whereas Assume is something that the static checker can rely upon, but it will not try to prove.

Here, I was talking specifically using verification terminology, where the difference is obviously night and day. Then you dismissed my post by claiming in D they are the same. You might as well declare that from now on true is the same as false in D and hence you can reach any desired conclusion, but that won't change my understanding of logic, nor would I applaud your design choice.


> At runtime Assert and Assume behave the same: If the condition is false, then the program fails – how it fails (e.g., throwing an exception, opening a dialog box, etc. can be completely customized with CodeContracts)."
> 
> Therefore after the Assert, the prover can assume the Assert condition is true. If the prover can prove the Assert is always true, the runtime check can be safely removed.

(Technically, probably no, as last time I checked, the code contracts prover still implicitly assumed there cannot be integer overflow.)

Maybe, but in D assertions get converted into optimizer assumptions in release mode _without_ any such proof being provided.

On 12.11.19 05:25, Doc Andrew wrote:
> ...
> Other languages are pretty clear on the distinction between assumptions and assertions. F* ("assume" - https://www.riseforfun.com/FStar/tutorialcontent/guide#h24) & SPARK ("pragma Assume" - https://docs.adacore.com/spark2014-docs/html/ug/en/source/assertion_pragmas.html) both make clear that assumptions are treated like axioms in their provers, and must be used with caution. The Boogie IVL ("assume" - http://chrisposkitt.com/files/teaching/SV-2015-AutoActiveVerification.pdf) works the same way.
> ...

Yup.

> Coq has no "assume" keyword, but the "assumption" tactic takes a hypothesis/premise and if it matches the goal (thing you're trying to prove/assert), then it solves the goal).
> ...

Sure, it is shorthand for "there is an assumption that proves the goal". This is a completely standard usage.

> Frama-C/ANSI C Specification Language ("assumes" clause - https://frama-c.com/download/acsl-1.14.pdf) just treats assumptions as hypotheses/premises that imply some conclusion, so pre-conditions, as far as I can tell. This might be where Walter is coming from in saying that Asserts and Assumes would be the same in D.

It is not. Walter is arguing about run-time semantics and he uses some weird argument ("-release only removes the check, it doesn't remove the assumption") to justify the unsafe behavior of asserts with -release.

> This is the only example I could find that uses "assume" like this, but there may be others.
> ...

The 'assumes' clause just says what assumptions are that the _function_ makes in order to satisfy the postcondition. It's saying "this function assumes ...", not "verifier, please assume ...". This is how preconditions operate. The function indeed assumes something, but it puts a burden on a caller who may not want to assume it.


> I think _most_ people consider Assert vs Assume the way SPARK and F* do - as seen here: https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/ 
> 
> 
> But hey, as Frama-C shows, it's not the only way to interpret those keywords.

Frama-C shows no such thing. I'm not confused at all by an 'assumes' clause in a function signature that signifies a precondition.

> The English language gets in our way sometimes. Inflammable = flammable, and all that.
> 
> If "assume" is taken to mean an "assert" which is a pre-condition,

Just to be clear: I have no problem at all with D's usage of 'assert' in preconditions. My point was that if you get rid of preconditions, 'assert' cannot express preconditions, so the prover won't know whether the callee or the caller is responsible for discharging a certain assertion.

> then fine, we could always point to Frama-C/ACSL to show that D isn't some insane outlier and that we aren't a bunch of backwards idiots.

The -release flag turns asserts into optimizer assumptions. In -release mode, a failing assertion in @safe code is undefined behavior. (In the C sense.) Assume cannot be @safe, while assert can, but Walter conflates them into the same construct.

> It wouldn't be the way _I_ would do it, but that's just one man's opinion, and I'm biased by my use of SPARK where pragma Assume has a clear meaning and works fine.
> 
> Given that we already have assert() in in{} contracts, to me the assume() keyword (in Walter's reckoning of the meaning) is redundant, and could be used for the axiomatic meaning.
> ...

Given that we have 'in' contracts, but we were arguing specifically about a scenario where we don't have them.

> If in{} and out{} contracts ever disappeared from the language, I think an external solver would need something like assume()/require() to distinguish preconditions from normal assertions.
> ...

Yes, this was exactly my point.

On 11/12/2019 2:26 AM, Timon Gehr wrote:
>> At runtime Assert and Assume behave the same: If the condition is false, then the program fails – how it fails (e.g., throwing an exception, opening a dialog box, etc. can be completely customized with CodeContracts)."
>>
>> Therefore after the Assert, the prover can assume the Assert condition is true. If the prover can prove the Assert is always true, the runtime check can be safely removed.
> 
> (Technically, probably no, as last time I checked, the code contracts prover still implicitly assumed there cannot be integer overflow.)

D doesn't have a contracts prover, and if it did, I think it would be a mistake to ignore integer overflow. What would be of value is being able to prove integer overflow does not happen. Note that the Value Range Propagation logic in D is able to do some nice work that does take into account overflows.

The global optimizer data flow analysis I wrote long ago would be broken if it didn't concern itself with overflows. In particular, loop induction variable optimization wouldn't work.


> Maybe, but in D assertions get converted into optimizer assumptions in release mode _without_ any such proof being provided.

True, but D doesn't have a prover anyway :-)

The user has complete control over whether asserts are checked at runtime or not. The thing about -release mode is the result of being bludgeoned in the press for having "slow" code because a competitor didn't generate the checks and the ignorant journalist did not understand this and did not ask before going to press.

I last tried Spark many years ago, and discovered its contract prover was so limited I concluded it had little practical value. (If I recall, it couldn't deduce things like odd and even.) I'm sure it has improved since, but how much, I have no idea.

On 11/12/2019 2:51 AM, Timon Gehr wrote:
>> If in{} and out{} contracts ever disappeared from the language, I think an external solver would need something like assume()/require() to distinguish preconditions from normal assertions.
>> ...
> 
> Yes, this was exactly my point.

The precondition would just be the sequence of assert()s before any other code, and the postcondition is the sequence that appears after any other code. It's not a challenge to pull that out of the AST.

On 12.11.19 12:35, Walter Bright wrote:
> On 11/12/2019 2:51 AM, Timon Gehr wrote:
>>> If in{} and out{} contracts ever disappeared from the language, I think an external solver would need something like assume()/require() to distinguish preconditions from normal assertions.
>>> ...
>>
>> Yes, this was exactly my point.
> 
> The precondition would just be the sequence of assert()s before any other code, and the postcondition is the sequence that appears after any other code.

I understand, and this strategy has the weaknesses I pointed out.

> It's not a challenge to pull that out of the AST.

Of course it is not challenging to implement. The point is that it is not a great idea, not that it is hard to do.

On 12.11.19 12:31, Walter Bright wrote:
> On 11/12/2019 2:26 AM, Timon Gehr wrote:
>>> At runtime Assert and Assume behave the same: If the condition is false, then the program fails – how it fails (e.g., throwing an exception, opening a dialog box, etc. can be completely customized with CodeContracts)."
>>>
>>> Therefore after the Assert, the prover can assume the Assert condition is true. If the prover can prove the Assert is always true, the runtime check can be safely removed.
>>
>> (Technically, probably no, as last time I checked, the code contracts prover still implicitly assumed there cannot be integer overflow.)
> 
> D doesn't have a contracts prover, and if it did, I think it would be a mistake to ignore integer overflow.

(Sure. Just saying that is what their prover does, so you actually can't eliminate the check based on that.)

> What would be of value is being able to prove integer overflow does not happen. Note that the Value Range Propagation logic in D is able to do some nice work that does take into account overflows.
> ...

(I know. I contributed some code to that.)

> The global optimizer data flow analysis I wrote long ago would be broken if it didn't concern itself with overflows. In particular, loop induction variable optimization wouldn't work.
> ...

It's funny you would bring that up, because it indeed does not work:
https://issues.dlang.org/show_bug.cgi?id=16268

> 
>> Maybe, but in D assertions get converted into optimizer assumptions in release mode _without_ any such proof being provided.
> 
> True, but D doesn't have a prover anyway :-)
> ...

Yes, it does, just not for functional correctness. D has a @safe fragment where the compiler automatically proves absence of memory safety problems. asserts are allowed in @safe code. Assuming incorrect propositions in your optimizer can cause memory corruption. See the problem?

> The user has complete control over whether asserts are checked at runtime or not.

No. You either check, or you risk UB. Complete control looks different.

> The thing about -release mode is the result of being bludgeoned in the press for having "slow" code because a competitor didn't generate the checks and the ignorant journalist did not understand this and did not ask before going to press.
> ...

Well, now you can be bludgeoned in the press for having "unsafe" code, because the ignorant journalist called into some library with an assertion in it. Even if they decide to ask, your response would make their article more juicy, not less.

> I last tried Spark many years ago, and discovered its contract prover was so limited I concluded it had little practical value. (If I recall, it couldn't deduce things like odd and even.) I'm sure it has improved since, but how much, I have no idea.
> 

I never tried Spark and it's entirely plausible that they were/are vastly behind the state of the art in verification research.

On Tuesday, 12 November 2019 at 11:31:43 UTC, Walter Bright wrote:
>
> True, but D doesn't have a prover anyway :-)
>

...yet :)

But in one sense, we already do. The run-time behavior of disabled assertions and checks basically just assumes you've worked through a "proof" of the program using your unit-testing.

>
> I last tried Spark many years ago, and discovered its contract prover was so limited I concluded it had little practical value. (If I recall, it couldn't deduce things like odd and even.) I'm sure it has improved since, but how much, I have no idea.

You might be asking too much from some of the solvers. It's worth slogging through some manual proofs with a proof assistant like Coq (highly-recommended resource: https://softwarefoundations.cis.upenn.edu/). After that, what an SMT solver is able to do on it's own seems very nice :)

Having said that, SPARK still requires a frustrating amount of hand-holding at times. You're able to do things like this now:

```
-------------------------------------------
-- double.ads (specification)
-------------------------------------------
package double
    with SPARK_Mode => On
is
    type SomeArrayType is array (Positive range <>) of Natural;

    function doubleArray(arr : in SomeArrayType) return SomeArrayType
        with
            Global => null,
            Depends => (doubleArray'Result => arr),
            -- set arbitrary range here in precondition to avoid overflow
            Pre => (for all idx in arr'Range => arr(idx) in 0..20000),
            -- prove that everything in the return array is even
            Post => (for all idx in arr'Range =>
                     isEven(doubleArray'Result(idx)));

    function isEven(num : in Natural) return Boolean with
             Contract_Cases =>
                 (num rem 2 = 0 => isEven'Result = True,
                  num rem 2 /= 0 => isEven'Result = False);

end double;

-------------------------------------------
-- double.adb (implementation)
-------------------------------------------
package body double is

    function doubleArray(arr : in SomeArrayType) return SomeArrayType with
        SPARK_Mode => On
    is
        doubled : SomeArrayType(arr'Range) := (others => 0);
    begin
        for i in arr'Range loop
            doubled(i) := 2 * arr(i);

            pragma Loop_Invariant(for all j in arr'First .. i =>
               doubled(j) = 2 * arr(j));
        end loop;

        return doubled;
    end doubleArray;


    function isEven(num : in Natural) return Boolean with
        SPARK_Mode => On
    is
    begin
        if num rem 2 = 0 then
            return True;
        else
            return False;
        end if;
    end isEven;
end double;

-------------------------------------------
-- main.adb
-------------------------------------------

with Ada.Text_IO;
with double; use double;

procedure Main
    with SPARK_Mode => On
is
    arr : SomeArrayType := (3, 7, 8, 0, 1);
    result : SomeArrayType := doubleArray(arr);
begin
     for i in result'Range loop
        Ada.Text_IO.Put(Integer'Image(result(i)) & ", ");
    end loop;
end Main;
```

The lame thing is the pragma Loop_Invaraiant. In order to be able to
make any conclusions about the array as a whole, you've got to explain how
the array looks at each point in the loop. Without that, the prover can't
prove that your post-condition is true. My understanding is that SPARK needs
a lot fewer of these than it used to, but it's still annoying.

Still, I think it's kind of neat that you can prove that kind of behavior at compile-time, no run-time checks or unit-tests required!

-Doc