community
community copied to clipboard
json-schema-org
GSoC: jsonschema.lean -- an implementation of JSON Schema in Lean
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
Hello @benjagm I would love to work on this, would you like to tell me how can i start with this
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.
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
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.
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!
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.
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
That's indeed the subject of this project yep! You of course do not to do it all ahead of time.
Got it but could you please explain what would I have to do right now as I am not getting clear from above
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
typekeyword, and get one test passing
Hey, This is Balraj, And I am willing to work on this project as a part of GSOC 2024
can you please guide me towards the 1st step that I can take in order to get involved in this project
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 ?
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 ?
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).
Thank you @Julian will start implementing right away ! any repo to be forked on to be worked with ?
also @Julian any slack channel / mailing list to be followed for further more conversation ?
Hy @Julian I am facing difficulty in containerizing lean and not finding any resources also could you suggest something
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.
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
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!