plans for network programming API

Stream: lean4

[Christian Pehle]

Currently there is no support for network programming, is that something that would eventually be supported by the standard library or should be contributed as third-party libraries?

[Sebastian Ullrich]

Lean 4 has been directly inspired by Rust in many regards, and the same can probably be said of its future standard lib size :) . So yes, a separate Lean package sounds like the more likely option at this point.

[Huỳnh Trần Khanh]

this might be tangential but does Lean 4 support some sort of asynchronous programming?

[Huỳnh Trần Khanh]

when there is I/O things must be either blocking or asynchronous right and I'd prefer asynchronous

[Marc Huisinga]

You can use tasks:
https://github.com/leanprover/lean4/blob/master/src/Init/Core.lean#L110
https://github.com/leanprover/lean4/blob/master/src/Init/System/IO.lean#L99

[Christian Pehle]

In fact I thought in line with https://doc.rust-lang.org/std/net/index.html, basically UDP, TCP, Sockets, etc., not higher level protocols.

[Sebastian Ullrich]

Oh, I didn't actually know that was there