## 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!