Stream: Program verification
Topic: API for Lean
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.
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
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?
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
Logan Murphy (Sep 16 2020 at 17:44):
Great. Thanks Simon!
Chris B (Sep 16 2020 at 19:55):
Rob Lewis made this playlist for LFTCM as well : https://www.youtube.com/watch?v=o6oUjcE6Nz4
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