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.