Rendered at 12:36:28 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
saviorand 3 days ago [-]
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
sroerick 11 hours ago [-]
amazing work
empath75 5 minutes ago [-]
I am currently working on a language compiler in lean and it seems to be fine, but compilation times are horrific and having a mathlib dependency just to build a programming language is a big ask for people.
OTOH, my borrow checker is provably sound, which is why I am using it.
solomonb 10 hours ago [-]
The secret of Lean4 is that its actually a great programming language, sort like a super Haskell. In fact I like it more as a programming language then as a proof checker!
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.
hiAndrewQuinn 3 hours ago [-]
This is terrific news. Last year I looked into Lean for generalist software development and found it was lacking quite a bit in the library department, so the news of e.g. leanpostgres being workable is a huge step forward.
slekker 5 hours ago [-]
Any performance benchmarks you could share? I think the trade-off for program correctness is worthwhile, but I wished to see more theorems around the core business logic
OTOH, my borrow checker is provably sound, which is why I am using it.
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.