Network (TCP/IP) and other IO

Stream: general

[Anton Parkhomenko]

Hi everyone!

I know almost nothing about theorem proving, but just discovered Lean 4 and absolutely felt in love with it - just what I was looking for when departing from Scala and Haskell. I want to try it out on some pet projects, but it seems that Lean is still very lean (no pun intended) on usual general purpose programming ecosystem (IO, parsers, DB connectors). Is there a centralized place (Zulip stream, Github repo) where people interested in making Lean approachable for mere mortals can ask questions and collaborate?

A more concrete question to the start the convo. Is it true that if I want to start writing TCP/IP API - I need to lean on (no pun intended) FFI (IO.FS and Socket.lean use FFI)? Is it possible to write FFI in Rust?

[Henrik Böving]

You can ask questions in #new members or #lean4 as much as you want.

And yes for any interaction with the operating system you do need FFI like in pretty much any language that is not C. That said I dont really understand what you mean by TCP/IP API? Sockets are the level of abstraction that an ordinary user is supposed to work with on basically any OS.

[Anton Parkhomenko]

To put it another way - if I want to write a connector to ZeroMQ (or Postgres or whatever or just do HTTP requests) - I need something to start with. And unlike Rust, Java, Haskell, where I can use a primitives like java.net.Socket - in Lean it has to be extern first. And from what I see these low-level primitives are missing or I was looking at the wrong places?

From what I see in IO.FS - Lean's FFI forwards function calls not directly to system calls, but to C++ function which makes the behavior more Lean-friendly.

[Henrik Böving]

Right. But we already have a working socket API here: https://github.com/hargoniX/socket.lean that you can just use, there is not much need to bother with implementing that again. That said HTTP is not implemented right now so one would have to start with that.

[Anton Parkhomenko]

Ok, cool. I haven't seen your socket.lean on reservoir (stumbled upon another implementation on Github, which is now deprecated). Also alloy looks very useful for the beginning.

[James Gallicchio]

not sure how much progress you made towards an Http library, but I have a bunch of the basic Http definitions/parsing implemented at https://github.com/JamesGallicchio/Http

[Anton Parkhomenko]

Hey @James Gallicchio! That looks great, I've also discovered Lurk Lab not long after starting this thread. But before that I and @Sofia Rodrigues have also started an Axiomed organization on github attempting to gather some engineering libraries there. I really would like to continue, but struggling to find time at the moment

[James Gallicchio]

Oh, that would be fantastic! That's what I spend most of my time working on at this point too :laughing: if you find time and would like to collaborate on things let me know :-)

[Anton Parkhomenko]

I highly recommend you to contact Sofia (here's her GH handle in case she didn't receive the notification: https://github.com/algebraic-sofia/) - I _think_ she currently has an ongoing web framework project outside of Axiomed