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

[benjagm]

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

Related issue in the JSON Schema project : https://github.com/json-schema-org/community/issues/606