Lean4 for Law

Stream: new members

[Jason Morris]

Hey. My name is Jason Morris, I'm working in the Canadian federal government on encodings of legislation to ensure legal software quality. Saw @Chris B do a presentation of using Lean 4 to verify the consistency of code with the corresponding law at ProLaLa on Sunday, and was impressed. Here to learn. Extremely limited functional programming experience (tried and failed to learn Haskell once), spend most of my time now in logic programming languages, and imperative microsimulation platforms. Noticing some opportunities to make small editing improvements to the documentation for Lean4. I'll take a look for a CONTRIBUTING. Any advice appreciated.

[Eric Taucher]

Jason Morris said:

My name is Jason Morris

When I read the title of the topic Lean4 for Law I thought, there is someone who is doing the same with SWI-Prolog using s(CASP), then I read your name.

Nice to see you hear.

[Floris van Doorn]

In case you hadn't found it yet, here is the relevant CONTRIBUTING for the Lean 4 doc:
https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md#documentation