Zulip Chat Archive

Stream: lean4

Topic: Coding with Lean 4

view this post on Zulip Henry Story (Jan 14 2021 at 11:16):

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...).

view this post on Zulip Alexander Bentkamp (Jan 14 2021 at 11:29):


view this post on Zulip Henry Story (Jan 14 2021 at 12:39):

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

view this post on Zulip Henry Story (Jan 14 2021 at 12:46):

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.

view this post on Zulip Henry Story (Jan 14 2021 at 13:07):

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

view this post on Zulip Henry Story (Jan 14 2021 at 13:41):

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.

view this post on Zulip Joe Hendrix (Jan 14 2021 at 21:53):

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.

view this post on Zulip Kevin Lacker (Jan 14 2021 at 22:51):

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.

view this post on Zulip Kevin Lacker (Jan 14 2021 at 22:53):

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

view this post on Zulip Henry Story (Jan 15 2021 at 03:40):

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.

Last updated: May 18 2021 at 23:14 UTC