Zulip Chat Archive

Stream: new members

Topic: Lean4 for Law

Jason Morris (Jan 19 2022 at 19:09):

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 (Jan 20 2022 at 07:51):

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 (Jan 20 2022 at 10:37):

In case you hadn't found it yet, here is the relevant CONTRIBUTING for the Lean 4 doc:

Last updated: Dec 20 2023 at 11:08 UTC