On 08.11.19 11:25, Walter Bright wrote:
> On 11/8/2019 2:09 AM, Timon Gehr wrote:
>> On 08.11.19 04:43, Walter Bright wrote:
>>> I don't see anything on that site that contradicts what I wrote. In particular:
>>>
>>> "Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art."
>>>
>>> is saying the same thing.
>>
>> Indeed, but more importantly, this group is working on verification techniques for unsafe Rust code, so it is likely that unsafe Rust libraries will be proved correct in the future.
> 
> I read it as ensuring the interface to the unsafe code is correct, not the unsafe code itself. I.e. "is properly encapsulated".
> ...

Read the next sentence after that. In general, feel free to read it any way you like, but that's not going to change the goals of the project, which correspond to my summary.

https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf

Last sentences in abstract: "Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem."

> After all, if the unsafe code can be proved correct, then it is no longer unsafe, and Rust's ownership/borrowing system can be dispensed with entirely as unnecessary for safety.
> ...

That stance makes little sense. The proofs are manual. As an analogy, it's a bit like saying "if it is realistic to audit @trusted functions, we can just mark the entire codebase @trusted, obtaining memory safe code without any of the @safe restrictions". The difference is that here, the proofs can be checked by the computer, but that doesn't make them much easier to provide.

> I'm happy to let the CS Phd's work on those problems, as I am way out of my depth on it.
> ...

I understand, but I can't help but notice that you often choose to contradict what they are saying on those issues anyway. The bird's-eye perspective you would get from an understanding of program verification and dependent type theory would help a lot for the design of sound and expressive type system extensions, such as O/B for D.

> I've convinced myself that the Ownership/Borrowing notion is sound, but have no idea how to formally prove it.
> ...

One way is to embed it into separation logic. It's in the paper below.

>> There is also this recent work on functional verification of safe Rust code: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:prusti.pdf 
>>
> 
> I don't see any reason why the techniques used in the paper wouldn't work on D,

Indeed, separation logic "works" on any language:
https://vst.cs.princeton.edu/download/VC.pdf
https://vst.cs.princeton.edu/veric/

The reason why you want both @safe and @system code is that most programmers are unable or unwilling to manually carry out memory safety proofs for all the code they write.

> given O/B.
> ...

Sure. Given O/B of the same caliber, you would get a similar simplification of correctness proofs. But right now we don't have correctness proofs at all, and a lot of times when program verification came up on this newsgroup it was rejected with a vague reference to the halting problem.

> Note that the paper says: "We do not address unsafe code in this paper".

(I'm aware, having read the paper. Which is of course why I described it as "functional verification of _safe_ Rust code". They also refer to RustBelt for verification of unsafe code.)

On Friday, 8 November 2019 at 03:43:56 UTC, Walter Bright wrote:
> On 11/7/2019 7:34 AM, Paolo Invernizzi wrote:
>> On Thursday, 7 November 2019 at 09:41:05 UTC, Timon Gehr wrote:
>>> On 07.11.19 08:34, drug wrote:
>>>> On 11/7/19 3:00 AM, Walter Bright wrote:
>>>>> Not that this is necessarily a bad thing, as I also promote the safe/unsafe code dichotomy.
>>>>>
>>>> And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
>>>
>>> http://plv.mpi-sws.org/rustbelt/
>> 
>> "... Any realistic languages targeting this domain in the future will encounter the same problem ..."
>> 
>> I underline _realistic_  ... Sorry Walter, I'm all with Timon on that.
>
> I don't see anything on that site that contradicts what I wrote. In particular:
>
> "Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art."
>
> is saying the same thing.

Agreed, and I definitely appreciate your effort in pushing towards mechanic verification on that topic.

What I mean is that there will be the need for manual verification also, when libraries will be forced to rely on unsafe code.

To my understanding, the project is providing guidance in doing that (manual) verification of unsafe code.

My advice is to work tightly coupled with Timon, to have a clear understanding of what is theoretically feasible and what not, for mechanical check, and to try to have clear borders around the two arenas.

In that way, you can concentrate on implementing and polishing what is pragmatically doable in the compiler, in a mechanical way, avoiding efforts towards dead ends.

But hey, you have already surprised us all when you designed D ... I will be glad to see that your idea really works!

/Paolo

On 08.11.19 11:11, Walter Bright wrote:
> On 11/7/2019 1:45 AM, Timon Gehr wrote:
>> That's not a plus. It will _mean_ something else. Therefore, you will have trouble at the interface between @live and non-@live code, because it is not the same language. Not to mention that @live without any further syntax changes will necessarily be even more restrictive than safe Rust.
> 
> I guess we'll have to see. I'm making progress every day on it. I'm looking forward to you tearing it apart :-)

So am I. I'm dispersing preliminary advice primarily to make that task more challenging. I'd be delighted to fail. ;)

On Friday, 8 November 2019 at 10:25:44 UTC, Walter Bright wrote:
>> 
>> Indeed, but more importantly, this group is working on verification techniques for unsafe Rust code, so it is likely that unsafe Rust libraries will be proved correct in the future.
>
> I read it as ensuring the interface to the unsafe code is correct, not the unsafe code itself. I.e. "is properly encapsulated".
>
> After all, if the unsafe code can be proved correct, then it is no longer unsafe, and Rust's ownership/borrowing system can be dispensed with entirely as unnecessary for safety.
>
> I'm happy to let the CS Phd's work on those problems, as I am way out of my depth on it.
>
> I've convinced myself that the Ownership/Borrowing notion is sound, but have no idea how to formally prove it.
>
>> There is also this recent work on functional verification of safe Rust code: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:prusti.pdf
>
> I don't see any reason why the techniques used in the paper wouldn't work on D, given O/B.
>
> Note that the paper says: "We do not address unsafe code in this paper".

The AdaCore/SPARK folks have done a lot of related work here that might be useful: https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memory-Management-in-Ada-and-SPARK.pdf

They took the pointer borrowing idea from Rust and plugged it into the SPARK solver (Why3) so formal correctness is guaranteed.

I am very bullish on formal verification in languages going forward. The one big advantage that D has in this arena is DbC. I was disappointed in your NWCPP talk that you listed it as a "miss." :) The potential here is huge! I think it's entirely possible that we can do _compile-time_ proofs that D contracts can be satisfied.

With sufficient pre & post-conditions on "unsafe" functions, (and maybe, as somebody pointed out, some asserts along the way to "nudge" the solver in the right direction), you can prove at that nothing bad happens with an automated solver. A couple of other contract types like loop & type invariants might also be necessary (they are in SPARK, at least). It would be pretty cool if you had to mark a function as unsafe only if the compiler (with some help) couldn't prove otherwise.

If Rust is going the route of a team of pros doing manual proofs in Coq to demonstrate absence of errors in "unsafe" code, they're in for a world of pain, frankly. My understanding is that the formal verification efforts in Rust were more geared towards proving that the Rust language/compiler themselves were sound, rather than giving Rust users a way of proving correctness of their own code, but I may be mistaken. The paper you linked shows the opposite, though.

I'm not an expert, and it's only a hunch, but I suspect that DbC + CTFE could make formal verification of D code a lot easier to implement than trying to graft it on to other languages. The PhD students can tell me if I'm wrong :)

My take is that formal verification is sort of where AI/ML was 20 years ago - academically interesting but of little practical use. Now it's a big deal, and I think in 10-20 years, FV will be too.

-Doc

On Friday, 8 November 2019 at 16:10:32 UTC, Doc Andrew wrote:
> With sufficient pre & post-conditions on "unsafe" functions, (and maybe, as somebody pointed out, some asserts along the way to "nudge" the solver in the right direction), you can prove at that nothing bad happens with an automated solver.

If you talk only about memory safety and require that programs are written in a certain way, then maybe yes.

In the general case this will not be possible though. You certainly need to manually guide the verifier (e.g. "nudge" the solver with asserts). The search space is vast. Keep in mind that when humans do proofs in math they do a lot of pattern matching, use a high level conceptualization of the problem space and only do it on "toy-sized" problems.

> I'm not an expert, and it's only a hunch, but I suspect that DbC + CTFE could make formal verification of D code a lot easier to implement than trying to graft it on to other languages.

Formal verification is never easy, but certainly less difficult when the programming language is designed with that in mind... D is too flexible.

And that's only for single-threaded programs. Add multi-threading and you basically need the programming language to be designed for it to get anywhere realistic. Such languages do exist, but they are not going to give you C-performance.

> My take is that formal verification is sort of where AI/ML was 20 years ago - academically interesting but of little practical use. Now it's a big deal, and I think in 10-20 years, FV will be too.

 I think FV is where AI was 70 years ago...

But yeah, maybe neural networks can be used for matching up verification problems with strategies so that the verifier succeeds more frequently, but the fact that an automated verifier frequently will fail to reach any conclusion will remain for practical programming that aim for very high performance in the forseeable future.

A more likely future is that processing performance will be in abundance and that you therefore don't have to write programs that maximize performance and can switch to languages and algorithms that are easier to prove correct...

On Friday, 8 November 2019 at 16:33:48 UTC, Ola Fosheim Grøstad wrote:
> On Friday, 8 November 2019 at 16:10:32 UTC, Doc Andrew wrote:
>> With sufficient pre & post-conditions on "unsafe" functions, (and maybe, as somebody pointed out, some asserts along the way to "nudge" the solver in the right direction), you can prove at that nothing bad happens with an automated solver.
>
> If you talk only about memory safety and require that programs are written in a certain way, then maybe yes.
>
> In the general case this will not be possible though. You certainly need to manually guide the verifier (e.g. "nudge" the solver with asserts). The search space is vast. Keep in mind that when humans do proofs in math they do a lot of pattern matching, use a high level conceptualization of the problem space and only do it on "toy-sized" problems.

Sure, one reason SPARK is amenable to FV is because the language restrictions and richness of Ada types does a lot to restrict that search space, the same way dependently-typed languages do.

>
>> I'm not an expert, and it's only a hunch, but I suspect that DbC + CTFE could make formal verification of D code a lot easier to implement than trying to graft it on to other languages.
>
> Formal verification is never easy, but certainly less difficult when the programming language is designed with that in mind... D is too flexible.

For sure - but there may be a _useful_ formally-verifiable subset of D buried in there somewhere, kind of like MISRA C.

>
> And that's only for single-threaded programs. Add multi-threading and you basically need the programming language to be designed for it to get anywhere realistic. Such languages do exist, but they are not going to give you C-performance.
>

With the way we do multi-threading now, where anything goes, absolutely. SPARK can formally verify multi-threaded tasks but using a fairly restrictive model (Ravenscar). I don't think performance goes absolutely in the tank with Ravenscar, but yeah, if you don't worry about synchronization, ignore race conditions, and just hope for the best, then sure, you're going to win in the benchmarks :)

I look at it a little differently - multi-threaded code is so tough to get right that some sort of verified correctness for it is becoming _essential_. (see: https://www.phoronix.com/scan.php?page=news_item&px=Google-KCSAN-Sanitizer)

It may be that a slightly-different threading model, perhaps like that thread "nursery" idea which has been posted here before (https://vorpus.org/blog/notes-on-structured-concurrency-or-go-statement-considered-harmful/) will be a magic bullet... or not.

>> My take is that formal verification is sort of where AI/ML was 20 years ago - academically interesting but of little practical use. Now it's a big deal, and I think in 10-20 years, FV will be too.
>
>  I think FV is where AI was 70 years ago...

Way too pessimistic! :)

>
> But yeah, maybe neural networks can be used for matching up verification problems with strategies so that the verifier succeeds more frequently, but the fact that an automated verifier frequently will fail to reach any conclusion will remain for practical programming that aim for very high performance in the forseeable future.

One thing that I've looked around for (without much luck) is just using GPUs to speed up the solvers themselves. Apparently parallelizing SAT solvers isn't the easiest thing in the world, but it would be a neat research topic.

>
> A more likely future is that processing performance will be in abundance and that you therefore don't have to write programs that maximize performance and can switch to languages and algorithms that are easier to prove correct...

The cool thing is that, with the right proofs in place, you can actually get _faster_ code when formally verified, because all of the normal sanity-checks you do in code can get shifted to compile-time. You might even be able to reduce  or eliminate thread blocking, etc. with the right model (and probably some HW assistance).

Your point is well taken, but I do hope that we can get proven correctness of bare-metal code without having to write something like Liquid Haskell ;)

-Doc

On Friday, 8 November 2019 at 17:07:59 UTC, Doc Andrew wrote:
> With the way we do multi-threading now, where anything goes, absolutely. SPARK can formally verify multi-threaded tasks but using a fairly restrictive model (Ravenscar). I don't think performance goes absolutely in the tank with Ravenscar, but yeah, if you don't worry about synchronization, ignore race conditions, and just hope for the best, then sure, you're going to win in the benchmarks :)

Ok, so Ravenscar requires tasks to be dispatched in a FIFO manner, but you should be able to do better than that if you only get to use high level synchronization.

For instance there are people who do verification of distributed communication protocols, so if you use some kind of message-passing scheme (or equivalent) then those approaches would apply.


> It may be that a slightly-different threading model, perhaps like that thread "nursery" idea which has been posted here before

«Structured concurrency» reminds me of rendezvous, i.e. that threads wait for each other at certain points, but less flexible.

I'm not really convinced that a "nursery" is easier to deal with than futures/promises, in the general case, though.


> One thing that I've looked around for (without much luck) is just using GPUs to speed up the solvers themselves. Apparently parallelizing SAT solvers isn't the easiest thing in the world, but it would be a neat research topic.

There are papers on it, but solvers are sensitive to the strategies (heuristics) used... so might be difficult to get right on a GPU. You'd probably have to use some kind of hybrid.

I also see that there are papers on FPGA SAT solvers.

> The cool thing is that, with the right proofs in place, you can actually get _faster_ code when formally verified, because all of the normal sanity-checks you do in code can get shifted to compile-time.

Sure, like indexing of arrays (array bounds checks).

> Your point is well taken, but I do hope that we can get proven correctness of bare-metal code without having to write something like Liquid Haskell ;)

Liquid Haskell looks interesting, though.  You might find this interesting:

http://leino.science/dafny-power-user/

It gives some hints of where such languages might go.

On Friday, 8 November 2019 at 17:07:59 UTC, Doc Andrew wrote:
> For sure - but there may be a _useful_ formally-verifiable subset of D buried in there somewhere, kind of like MISRA C.

I guess it is worth mentioning though that all integers in D follow the semantics of modular math, so you would not be able to conduct proofs with the assumption that you work with natural integers. So you cannot assume that "x+1 > x" for any type in D, that might make many proofs more difficult.

Modular math can be handled with bit-blasting (turning each bit to a logic expression and use SAT), but maybe with less success.

On Friday, 8 November 2019 at 17:41:06 UTC, Ola Fosheim Grøstad wrote:
>
>> Your point is well taken, but I do hope that we can get proven correctness of bare-metal code without having to write something like Liquid Haskell ;)
>
> Liquid Haskell looks interesting, though.  You might find this interesting:
>
> http://leino.science/dafny-power-user/
>
> It gives some hints of where such languages might go.

Thanks for the link! I've looked briefly at Dafny in the past and liked what I saw. Between Dafny, F* and the Lean prover, MS research is doing some pretty neat work in the field.

On Friday, 8 November 2019 at 17:55:41 UTC, Ola Fosheim Grøstad wrote:
> On Friday, 8 November 2019 at 17:07:59 UTC, Doc Andrew wrote:
>> For sure - but there may be a _useful_ formally-verifiable subset of D buried in there somewhere, kind of like MISRA C.
>
> I guess it is worth mentioning though that all integers in D follow the semantics of modular math, so you would not be able to conduct proofs with the assumption that you work with natural integers. So you cannot assume that "x+1 > x" for any type in D, that might make many proofs more difficult.
>
> Modular math can be handled with bit-blasting (turning each bit to a logic expression and use SAT), but maybe with less success.

It works if you explicitly mark overflow as an error. You can try to prove that x <= x.max for a given path, and if you can't, then you just flag a warning. That's what SPARK does, at least. If the modular arithmetic is desired you'd probably have to manually put the overflow check and reassignment to 0 (or whatever) in there.

That's one kind of annoying thing I discovered about Rust when working on some crypto code - having to write Wrapping types all over the place. The bad thing there was that the overflow checks were only in Debug mode, so in Release mode the code worked as intended without Wrapping. That was a few years ago, so things may be a little different now.