Zulip Chat Archive

Stream: Program verification

Topic: API for Lean


view this post on Zulip Logan Murphy (Sep 16 2020 at 16:32):

So my medium-term goal is to build an API which can take some strings representing fragments of a model (e.g. in a translation of the GSN), plug those into some functions in Lean, and observe whether the program type-checks or throws some error.

I don't think there's much documentation out there about using Lean this way, but if anyone knows of any projects that use Lean for verification in a similar way that I could refer to to start piecing something this together, that would be great! I'm still a bit new to verification so apologies if any of this seems silly.

view this post on Zulip Simon Hudon (Sep 16 2020 at 16:46):

There is a C API . I haven't used it but that fits your description. I'm not sure if that's going to be the tool that you want. You might be better off trying to parse GSN using Lean meta programming and generating definitions. This way, if you can't automate all the relevant proofs, you can still use Lean to discharge them

view this post on Zulip Logan Murphy (Sep 16 2020 at 17:35):

Interesting. I've so far not done much meta programming in lean. I see that there's a chapter on it in the Hitchhiker's Guide, and a small section in Programming in Lean. Any other references that you know of?

view this post on Zulip Simon Hudon (Sep 16 2020 at 17:41):

There's this here https://leanprover-community.github.io/learn.html#metaprogramming-and-tactic-writing and otherwise people on Zulip are usually pretty responsive

view this post on Zulip Logan Murphy (Sep 16 2020 at 17:44):

Great. Thanks Simon!

view this post on Zulip Chris B (Sep 16 2020 at 19:55):

Rob Lewis made this playlist for LFTCM as well : https://www.youtube.com/watch?v=o6oUjcE6Nz4

view this post on Zulip Chris B (Sep 16 2020 at 20:00):

This shows some really basic IO stuff like reading input and printing to the command line : https://agentultra.github.io/lean-for-hackers/


Last updated: May 08 2021 at 23:10 UTC