GSoC: jsonschema.lean -- an implementation of JSON Schema in Lean

[Julian]

Project title

jsonschema.lean -- an implementation of JSON Schema in Lean

Brief Description

Lean is an extremely interesting and up and coming programming language created by Leo de Moura (formerly at Microsoft Research, now at Amazon) and his team. It is an "interactive theorem prover", though for our purposes what it offers is in short an ability to write a piece of software and then have the ability to formally prove properties of the software that you've written, all within the language itself ("software verification").

Let's write an implementation of JSON Schema in Lean!

Why? Here are some reasons:

• because every language needs a JSON Schema implementation, and Lean doesn't yet have one!
• having an implementation in Lean would enable work on formal verification! This would enable us or others to formally prove theorems about JSON Schema within our implementation
• it will probably be fun! Lean is a relatively young language, so we'll be able to "kick its tires" a bit

Expected Outcomes

• A new repository containing a new Lean JSON Schema implementation, with as many keywords implemented as we have time for for a single dialect of JSON Schema
• Integration of this implementation with Bowtie

Skills Required

• Desire to learn a new programming language!
• Some experience with functional programming a big plus (e.g. Haskell, F#)
• Basic knowledge of JSON Schema

Mentors

@Julian

Expected Difficulty
Hard

Expected Time Commitment
350 hours

[PRANJALRANA11]

Hello @benjagm I would love to work on this, would you like to tell me how can i start with this

[Julian]

Great! A good first step is to review:

• a basic JSON Schema tutorial, which you can find on our website
• a basic Lean tutorial, which you can find on the Lean website
• an existing JSON Schema implementation's documentation, which you should do after understanding what JSON Schema is for -- try one and see if you can get it to perform some validiation for you.

Good luck, feel free to follow up with specific questions.

[Sandhu-Sahil]

Hi @benjagm @Julian ,
I have read the project requirements and am interested to work on the same, I am ready and excited to new programming language and also I have hints of functional programming, what is it and how it works not in Haskell or F# But that I am also willing to learn, it will hardly take 1-2 weeks.

would you like to tell me how can i start with this, and what are prerequisite for this

[vibhu1805]

Hi @Julian @benjagm , I am also interesed in working on this issue and willing to learn new programming language and all the above mentioned prerequisites.

[doorkn-b]

Hello @Julian. I'm really interested in getting involved with this project.

I have a good amount of experience with Haskell. I have been a TA for the course INF1A (INFR08025) at The University of Edinburgh tutoring Haskell and Computational Logic to around 40 students.

I also have some experience with interactive theorem provers and formal verification in Lean, Agda and Nuprl (particularly procedural proof scripts).

I was successful in being able to validate a few JSON files against it's schema. I'd love to tackle implementing a basic schema feature-- perhaps type validation for a few cases?

Any advice from your side on how I can proceed with better enabling myself for this would be much appreciated.

A little more information about the current priorities within the project would also be great.

Thanks a bunch!

[Julian]

Fantastic! Hi (to you and everyone).

I was successful in being able to validate a few JSON files against my schema. I'd love to tackle implementing a basic schema feature-- perhaps type validation for a few cases?

This sounds like a very good first thing to try!

Another recommendation I would have is to immediately try to write a Bowtie harness. A tutorial for doing that is here but obviously write it in Lean not Lua. You'll immediately fail every test of course, but that's a good qualification task for this issue! Write a Bowtie harness in Lean, fail every test, get 1 to pass, and yes type I think is a good easy one.

[PRANJALRANA11]

Hy @Julian I have seen the tutorials and tried Bowtie with Lua and I have some questions 1 do I first need to write a JSON implementation in Lean and then integrate it with Bowtie or I am doing it wrong

[Julian]

My recommendation was:

• Start a new empty Lean project
• Write a small Bowtie harness in Lean using the tutorial I linked, which should be a few hundred lines of code
• That harness will fail every test because you haven't implemented any functionaity
• Then you can pick the simplest possible part of JSON Schema to start, perhaps the type keyword, and get one test passing

[BalrajDhakad]

Hey,
This is Balraj,
And I am willing to work on this project as a part of GSOC 2024

[lgsurith]

Hey @Julian i would love to learn more about the Lean codebase and try to contibute for the raised issue ! , any pre-requisites that i must do before moving forward with the given issue ?

[Julian]

Great! Glad to hear. None other than what's mentioned above!

[lgsurith]

Sure @Julian will start implementing right away and update you on the tasks that i complete !
Quick question are those a part of qualification task ? and also i am pretty new in the world of FOSS development so will it hinder me in any chance of getting qualified ?

[Julian]

Quick question are those a part of qualification task ?

For this project yes!

and also i am pretty new in the world of FOSS development so will it hinder me in any chance of getting qualified ?

Not at all, you are very welcome, and indeed the program is tailored just for people who are! (Of course that doesn't mean you're guaranteed! But you are in the right place).

[lgsurith]

Thank you @Julian will start implementing right away ! any repo to be forked on to be worked with ?

[Julian]

Not yet! Feel free to create one for your own work.

[lgsurith]

Alright ! Thanks @Julian .

[lgsurith]

also @Julian any slack channel / mailing list to be followed for further more conversation ?

[PRANJALRANA11]

Hy @Julian I am facing difficulty in containerizing lean and not finding any resources also could you suggest something

[Julian]

also @Julian any slack channel / mailing list to be followed for further more conversation ?

There's a JSON Schema slack for our community. There's also a Lean Zulip for the Lean one.

Hy @Julian I am facing difficulty in containerizing lean and not finding any resources also could you suggest something

Hard to say without any information. The only thing I immediately know to tell you is that if you're using alpine, that's a MUSL based image, and Lean I think is less happy with MUSL than Glibc. But you should definitely be able to find some existing people containerizing Lean, I've seen it before on the Zulip certainly.

[lgsurith]

Hey @Julian i might have gone through Docs and implemented basics , can you guide me on the second part because i am completely lost on that part.
Github Repo for Reference : https://github.com/lgsurith/JSON_SCHEMA_LEAN

[Julian]

I can't be more specific than that for now I'm afraid, what you have there isn't a Lean project. It might be this specific project doesn't precisely suit your skills as I'd want you to figure out how to at least get the qualification task done on your own without much help! There's no shame though if that's the case, there are other projects within the organization which may be a better fit!

[lgsurith]

Alright will try my best to figure it out !

[ashutosh7i]

Hello @Julian ,
i read project description, then i also read Lean documentation thoroughly,
i personally am not convinced on why we should have a JSON implementation for Lean,
initially i was very excited to implement, i explored and learnt Lean a bit, but then i got several questions in my mind.

we sure can implement a json lib for Lean,
but who/how will someone use that for?

according to my research Lean is a "interactive theorem prover", its docs talks through language basics and tooling,
we as devs use JSON for data communication over(or) network but since i say Lean mostly working on cli,
How exactly someone will use our JSON lib for ??
I personally am excited to work on it, just need some clarification.

Thanks and regards,
Aashutosh soni

[Julian]

It's slightly hard to parse your message since I think there are some typos, but I'll assume you mean "a JSON Schema implementation for Lean" rather than "JSON" in both places?

There's a brief answer to that in the issue description. Some additional answers to:

but who/how will someone use that for?

Users of Lean for one, and people interested in formally proving things about JSON Schema for another!

we as devs use JSON for data communication over(or) network but since i say Lean mostly working on cli,
How exactly someone will use our JSON lib for ??

Lean is a normal programming language, so you can write programs that do whatever you'd like in it, though yes I don't know of someone using it to build what it sounds like you have in mind, namely "traditional web APIs" -- but that's just one use of JSON, it's used in many places, and very much not just for APIs over the network, even aside from Lean. It's used e.g. for serialization of datasets, to name one example. And anywhere there's a need for JSON, there's a likely need for JSON Schema.

[ashutosh7i]

Thanks for your reply and clarification @Julian 😄.

Sure there can be other use cases for "a JSON Schema implementation for Lean"
Best of Luck🎉.

[PRANJALRANA11]

Hy @Julian I have containerized the lean app and am able to take the std input from Bowtie but for returning a JSON response i was not able to find any library as i can't directly write json in lean

[Julian]

It's a module in Lean's standard library: https://github.com/leanprover/std4/blob/main/Std/Lean/Json.lean (and really is partially in "Lean Core") -- which shouldn't have been impossible to find :), but hopefully that helps.

[benjagm]

Thanks a lot for joining JSON Schema org for this edition of GSoC!!

Qualification tasks will be published as comments in the project ideas by Thursday/Friday of this week. In addition I'd like to invite you to a office hours session this thursday 18:30 UTC where we'll present the ideas and the relevant date to consider at this stage of the program.

Please use this link to join the session:
🌐 Zoom
📅 20124-02-29 18:30 UTC

See you there!

[CAIMEOX]

Hello @Julian
I have read the requirements and comments in this issue. This project idea is very interesting and I'm glad to participate.

I'm a fan of functional languages and theorem provers, and have working with OCaml for a long time. And I have been studying theorem provers (including lean4) and type theory for the past year and I think it's time to use them to write some projects.

In the past two months I've been working with a project program that turns simple json schema into typescript type declarations so I'm familiar with basic knowlegde about json schema.

I have gone through the Docs in bowtie website and implemented basic bowtie protocol in my repo.

Thanks and regards.

[Infinity-code]

Hello @Julian. I am interested in this project.
As a budding mathematician, I had heard about Lean when some tough theorems were validated. I would like to take this opportunity to learn Lean and contribute to this project.

[adwait-godbole]

Planning to tackle this one in GSoC 👍!

[Julian]

Cool! A reminder here just to make sure not to confuse things with the Bowtie tickets -- the qualification task on this issue is this one i.e. to start a Lean project and write a Bowtie harness in Lean which fails all the tests!

[PRANJALRANA11]

Hy @Julian I had written the bowtie harness which is failing the test is this enough to pass the qualification task

[Julian]

Great!

[Arnav-99]

Hello @Julian, I'd like to contribute to this project.

I have a year of experience in Lean 4 and am currently working on adding greater user support for co-inductive types. I'd love to channel this experience into a community-wide project!

Additionally, please correct me if I'm wrong, but this https://json-schema.org/blog/posts/bowtie-intro is the link to the JSON schema tutorial right?

Thanks!

[Julian]

Hi. Nice! Welcome. Thanks for your interest!

Additionally, please correct me if I'm wrong, but this https://json-schema.org/blog/posts/bowtie-intro is the link to the JSON schema tutorial right?

That's an intro post which might be worth skimming, the actual harness tutorial is here!

[Arnav-99]

I'm experiencing difficulties installing Bowtie using brew on Ubuntu 20.04, any ideas why this might be occurring?

I have Python 3.12, and attached herewith is the brew output. Assistance would really help, thanks!
brew_out.txt

[Julian]

You're the first person to try to install it via brew on Linux I suspect (and honestly the first person I've ever met who uses brew on Linux :).

It's not clear whose fault it is from that error message (whether something's broken in Linuxbrew or in Bowtie's formula).

I'd recommend installing it via pipx to get unblocked.

[Arnav-99]

Alright, I will try that! Just to clarify, the pipx installation guide be carried out by substituting podman with Docker right? (It seems that the former is not compatible with versions older than Ubuntu 20.10 but the latter is)

[Julian]

I would expect that to be fine yeah.

[benjagm]

🚩 IMPORTANT INSTRUCTIONS REGARDING HOW AND WHERE TO SUBMIT YOU APPLICATION 🚩

Please join this discussion in JSON Schema slack to get the last details very important details on how to better submit your application to JSON Schema.

See communication here.