API for Lean

Stream: Program verification

[Logan Murphy]

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]

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]

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]

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]

Great. Thanks Simon!

[Chris B]

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

[Chris B]

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