saviorand

I wanted to know if Lean 4 is usable for an everyday web app yet, not just for proofs, so I built RealWorld (the Medium clone) in it, frontend included, using Datastar. Looks like it's feasible now with the new libraries. This post describes the experience

True, although I think they're working on support for generic effects

Function call always returns, and to one single caller, whereas effects can choose not to "return" at all, resume multiple times, etc

Koka, Effekt and 4 other research languages are mentioned earlier in the article though? This talks about practical languages, not research-only

Can confirm this is a good book -- I've been subscribed to the newsletter for a while

I’m usually entering contractor agreements (as a contractor) — guess I don’t need to generate one but might be good to have some kind of support when reading, like a way to compare different agreements and pick the best terms

This is good! I need NDA’s fairly often at work and here it’s quick to make one

Wow, thanks. Live and learn. Does the way some tools check whether the email was read by the recipient or not have something to do with this structure, too?