Zulip Chat Archive

Stream: general

Topic: Rust verification working group

Simon Hudon (Apr 15 2018 at 18:31):

Did anybody else see this:

https://github.com/rust-lang-nursery/wg-verification
https://gitter.im/rust-lang/wg-verification

There seems to be an official verification working group for Rust. It might be a great opportunity to promote Lean

Moses Schönfinkel (Apr 15 2018 at 18:56):

I think Lean is not quite there yet :(. (Mostly due to stability.)

Simon Hudon (Apr 15 2018 at 19:31):

You think we should just wait before getting started in that direction?

Moses Schönfinkel (Apr 15 2018 at 19:32):

I do. I have a feeling that Rust wants something more... ready?

Simon Hudon (Apr 15 2018 at 19:33):

That makes sense but my impression from the group is that there is a wide variety of approaches. The Iris / RustBelt project seems to be the major one but they seem to encourage diversity rather than try to settle on a single verification approach

Moses Schönfinkel (Apr 15 2018 at 19:35):

Perhaps you're right. I think Jared contributes to Rust so mayhap he's already brought it to their attention then?

Moses Schönfinkel (Apr 15 2018 at 19:35):

Btw, in spite of the fact that I've been writing Lean exclusively for a few months now (and dropping Coq), if I were to start an industrial project right now I would choose Coq.

Simon Hudon (Apr 15 2018 at 19:37):

That makes sense. The infrastructure is far more mature. I think it will take a while for Lean to catch up. It seems to me that 1) it can happen and 2) when / if it does, Lean will be a more approachable solution to start hacking with.

Moses Schönfinkel (Apr 15 2018 at 19:38):

I completely agree. Really the notation is just more important than the Coq community realizes and Lean has just the right amount (as opposed to Agda who have gone way too far in the notational direction).

Simon Hudon (Apr 15 2018 at 19:40):

I agree. I feel like organizing the libraries around type classes instead of module / functor also makes them far more usable.

Simon Hudon (Apr 15 2018 at 19:41):

I guess the point of already starting on verification project is slowly catching up to the Coq infrastructure

Simon Hudon (Apr 15 2018 at 19:41):

I wonder if it's realistic to hope for a sort of FFI between Lean and Coq

Moses Schönfinkel (Apr 15 2018 at 19:41):

Typeclasses are sweet. Also I've grown accustomed to using the decidable trick to use the same function in decidable and potentially undecidable contexts. It's so awkward to always do if band in Coq. (Although I believe Lean wants to actually drop this particular use case? Which is saddening.)

Moses Schönfinkel (Apr 15 2018 at 19:42):

I want FFI to C, Idris style.

Simon Hudon (Apr 15 2018 at 19:43):

It's so awkward to always do if band in Coq.

YES! It took me a while to appreciate that but it's incredible.

Simon Hudon (Apr 15 2018 at 19:45):

Although I believe Lean wants to actually drop this particular use case?

Are you referring to ite taking a bool instead of a decidable Prop? I think all that it will do is shift the use of decidable from ite to the coercion from your proposition to bool. I think it's too useful and pretty to drop.

Moses Schönfinkel (Apr 15 2018 at 19:45):

Oh, yes I was referring to that but clearly I had misunderstood then.

Moses Schönfinkel (Apr 15 2018 at 19:45):

So we're keeping the trick.

Simon Hudon (Apr 15 2018 at 19:46):

I want FFI to C, Idris style.

Multiple FFIs might be required. Specifically, a FFI to Coq would be really cool if it allowed us to reuse Coq theorems and tactics. That might mean we can use Iris in Lean for example.