Coding with Lean 4

Stream: lean4

[Henry Story]

I am just wondering how far off it is to be able to build web servers in Lean 4, or perhaps produce code that can be used by, say, Rust based web servers... Where would it make most sense to use it? (I am having to build a web server right now, so I am looking around...).

[Alexander Bentkamp]

https://youtu.be/TgHISG-81wM?t=2932

[Henry Story]

Thanks that is very interesting. I just looked at it again. (Had seen in 2 months ago).

[Henry Story]

My use case is that I need to write an implementation of Tim Berners-Lee's Solid Server, especially the access control part, which requires integrating RDF parsers and reasoning ( in Category Theory RDF graphs are Functors from Bicategories of Relations to Rel, and reasoning are natural transformations (I think)). Though these need to be extended to quads... That means one has to fetch data from the worldwide data store called the World Wide Web, check access control rules for each resource, verify credentials, etc... One needs HTTP/2.0 for efficiency, and a number of other things.

[Henry Story]

As lean compiles to C I guess integration with Rust would be the easiest.

[Henry Story]

That raises the question as to what type of work would be best done in Lean, and what would be best left to Rust. I guess that will develop over time, as Lean evolves.

[Joe Hendrix]

I have very little Rust experience, but I'd be interested in seeing what you learn from this. It's somewhat tedious but otherwise straightforward to create Lean APIs that invoke existing C/C++ code with some glue code interacting with the Lean runtime C API.

[Kevin Lacker]

RDF parsers and general web tools are going to be more fully developed in Rust than in Lean 4. probably even more developed in the more popular languages like javascript or python rather than rust, if you aren't set on rust per se.

[Kevin Lacker]

my suggestion is to do as much as you can in rust and then pop over to lean if some component (functors? bicategories? i dunno what that stuff is for but maybe lean is extra good at it) is a lot easier to do in lean

[Henry Story]

There is some interesting work indeed on Rust and RDF see eg. WasmTree: Web Assembly for the Semantic Web, which points to where things are going I think.

(I am coming from Scala/Scala-JS background which I know well, but as I am on a new project, there is potential to switch, so I am looking around. Rust also has HTTP/2.0 implementations which must have been a lot of work to implement. The Scala Akka framework is only now finishing support for those.)

Also am very intrigued by what the future holds for programming using proof assistants, especially with HoTT allowing one to transport proofs between types. As I am building a security platform, being able to produce proofs of the correctness of the code, would be very advantageous.