November 10, 2019
On Sunday, 10 November 2019 at 02:51:53 UTC, Doc Andrew wrote:
> I think you'd just have to wait until all the CTFE and template stuff is done before you start generating VCs. It might not be a deal-breaker, but that's speaking from ignorance, frankly.

Also keep in mind that you have to deal with exceptions, so you have to introduce a lot of branching code (unless the verifier does that rewriting for you).

> Oh I dunno, aside from adding some extra contracts and avoiding certain language constructs* (like goto), not much really has

You can allow gotos (at least the most common usage). Deal with it the same way you model exceptions.

> * Granted, those "certain language constructs" may end up being an insurmountable barrier, where the formally verifiable subset of D is stripped of so many features that it isn't really worth it. Too early to tell.

Well, I think that modular ints is an issue that may make some cases harder, but I think most constructs can be modelled in a VC language. Still a lot of work.

November 10, 2019
On Sunday, 10 November 2019 at 04:15:08 UTC, Doc Andrew wrote:
> Option 2, taken by Dafny and SPARK (and I think FRAMA-C too, but don't quote me on that), is take the language you want (or at least something close), then generate an intermediate language that can be easily broken down into verification conditions to run through the solver.
>
> For formally-verified D, this is the route I'd want, because I like writing D!

Sounds like you have set a course that you can follow!

I would personally just have ignored templates and extended one of the linty D-parser, as I think it will lead to a more transparent codebase that is easier to experiment with than modifying the D compiler.

But maybe you'll find that doing it within dmd from start works out for you. The plain dmd compiler should not so difficult to set up, so just try it, I guess?

You could build your own VC-ast from the D-ast, then manipulate it and emit VC-code.

> That's an almost criminally-understated view of the task, but I think it might give D a path towards FV, if people think it's worth it.

Yes, I don't know,  what is most important is that you think it is important enough to carry the burden on your own for at least a year. Over time, surely others will come along that share that viewpoint. Just keep the codebase simple so that people with no FV knowledge can contribute... In the beginning there will basically be no advantages to using the tool, so... it takes a lot of patience.

Maybe a well written DIP can bring people on board from the start, but I haven't seen many people interested in FV when that topic has been discussed in the forums. Again, just try, I guess?

November 10, 2019
On Sunday, 10 November 2019 at 10:22:27 UTC, Timon Gehr wrote:
> - Modular verification means it's enough to have DI files for functions you call, without a function body.
>
In a unit testing world, every assert gets checked every time the function is called anyhow, so it makes little difference whether they are pre or post-conditions, or just sprinkled throughout a function.

In a verified world, it makes a _huge_ difference. A verified function with an "in" contract states, "this function satisfies all of its contracts (explicit and implicit) _if and only if_ the in contracts/preconditions are satisfied".

With this, once that function is verified,
a caller need only make sure that it satisfies those preconditions at each call site. In the absence of preconditions, the verifier has to re-prove _every_ assert() in the callee function (and every OTHER function that the callee uses too...) _every time_ it's called throughout the program. It's an exponential increase in the problem space.

You _might_ be able to do a flow analysis to suss out which asserts are considered preconditions without explicitly stating so, but it seems like a tough problem, and explicitly stating them seems like a better practice anyhow.

Modular verification is really the only tractable way to approach the problem. You build up the proof starting from leaf functions which, once proven, need only their pre-conditions checked at subsequent calls. Globals and functions with side-effects complicate this somewhat, but for pure functions it works very cleanly.

And like Timon said, in the absence of in/ out contracts in a .di file, verified libraries provide no way to extend their guarantees to the user.

-Doc

November 10, 2019
On Sunday, 10 November 2019 at 13:39:23 UTC, Ola Fosheim Grøstad wrote:
> You can allow gotos (at least the most common usage). Deal with it the same way you model exceptions.

https://www.google.com/search?q=transformation+goto+eliminiation

November 10, 2019
On Sunday, 10 November 2019 at 10:53:38 UTC, RazvanN wrote:
>
> At UPB Bucharest we have discussed with a formal verification professor and published a research project for a masters student (2 years) where the goal is to implement a simple solver for contracts in D.

Very cool! Do you know if there is a link or any publications (even if it's just a proposal) for the research?

-Doc
November 11, 2019
On Sunday, 10 November 2019 at 20:02:33 UTC, Doc Andrew wrote:
> On Sunday, 10 November 2019 at 10:53:38 UTC, RazvanN wrote:
>>
>> At UPB Bucharest we have discussed with a formal verification professor and published a research project for a masters student (2 years) where the goal is to implement a simple solver for contracts in D.
>
> Very cool! Do you know if there is a link or any publications (even if it's just a proposal) for the research?
>
> -Doc

Unfortunately, I do not know the site where it has been published, but the proposal is in Romanian anyway. What I know is that the student will have to do a state of the art review in verification techniques and come up with a proposal. The milestones are:

1. State of the art review
2. Implement one of the existing techniques
3. Come up with an enhancement of some sort.

We don't know yet the exact details, but we are confident that at least we can implement something that is already out there.
November 11, 2019
On 11/10/2019 2:22 AM, Timon Gehr wrote:
> On 10.11.19 00:23, Walter Bright wrote:
>> On 11/9/2019 4:23 AM, Timon Gehr wrote:
>>> You need in and out contracts for modular verification.
>>
>> You can pick up both from looking at the assert's in the prolog and epilog of the function.
>> ...
> 
> - Modular verification means it's enough to have DI files for functions you call, without a function body.

I know.


> - Some asserts in the prologue of your function might really be asserts and not assumes.

The distinction between assert and assume has come up before, and I've argued that in D they are the same.


> - Similarly, some asserts in the epilogue of your function might not be things you actually want to guarantee to the caller.

You could look for this pattern:

  T biff(P p)
  {
     assert(something about p);
     T result;
     scope (success) assert(something about result);

     ... function body ...
  }

and have the contracts.


>> More importantly, nobody is working on a modular verification system for D, and haven't for 20 years, so the contracts aren't particularly useful.
> Programmers can read contracts too, not just verification systems. They are useful documentation and can be used for assigning blame: Is the assertion failure the fault of the caller or the callee?

I do understand the point of them. I've been enamored with contracts for 20-30 years. I've done presentations promoting them. I added them to my C++ compiler. I added them to D.

I just haven't found them particularly useful or helpful when I've tried them.
November 11, 2019
On Monday, 11 November 2019 at 10:39:24 UTC, Walter Bright wrote:
> The distinction between assert and assume has come up before, and I've argued that in D they are the same.

assert:   if(failure) exit…
assume: if(failure) unreachable…

Can't be the same…

> I do understand the point of them. I've been enamored with contracts for 20-30 years. I've done presentations promoting them. I added them to my C++ compiler. I added them to D.
>
> I just haven't found them particularly useful or helpful when I've tried them.

They are most useful when you try to learn complex third party libraries.

November 11, 2019
On Monday, 11 November 2019 at 10:39:24 UTC, Walter Bright wrote:

> I just haven't found them particularly useful or helpful when I've tried them.

There are two problems with contracts in D.

1. In-contracts are executed by the callee instead of the caller. Currently there's only a syntactic difference between an in-contract and a regular assertion inside the function body.

2. Phobos is not shipped with assertions enabled. There should be a debug version of Phobos shipped with DMD with assertions enabled. Perhaps that could be linked by default when the `-debug` flag is used.

Related issues:

https://issues.dlang.org/show_bug.cgi?id=6549
https://issues.dlang.org/show_bug.cgi?id=12344
https://issues.dlang.org/show_bug.cgi?id=19131

--
/Jacob Carlborg
November 11, 2019
On 11.11.19 11:39, Walter Bright wrote:
> 
> 
>> - Some asserts in the prologue of your function might really be asserts and not assumes.
> 
> 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.