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 21 hours ago [-]
amazing work
solomonb 20 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.
adamddev1 9 hours ago [-]
Any experience with Rocq? I've been curious about jumping into dependent types.
nextaccountic 23 minutes ago [-]
another one that seems practical, but I never tried, is F* (Fstar)
embedding-shape 9 hours ago [-]
> The secret of Lean4 is that its actually a great programming language
Kind of feels like you have to specify for what here, as no programming language is just "great at everything", they all have their places (except Clojure and children which is great at everything obviously). Say I run shell commands, obviously a PL based around proofs will be way too much, compared to if I want to create aircraft stabilizer with movable control surfaces.
nixie-tubes 7 hours ago [-]
Nice! A bit back I did some experiments with converting some web code from TypeScript to Idris 2 and seemed to work out well.
However, after some consideration I opted to not move forward with it just yet. The problem is that at least for that particular case I could only really practically prove some properties of the code. With more time I could perhaps bring it up further. So for entirely practical reasons I am still going to want tests for the rest of the code. And while Idris 2 does have support for testing and continuous integration, at that time there were no solutions for measuring test coverage or performing mutation testing.
It does seem like since then someone has created a coverage tool for Idris 2, but mutation testing tooling still doesn't exist.
Lean 4 doesn't seem to have anything for coverage yet. I found some tool that claims to do a kind of mutation testing for Lean 4, but it sounds like it is still quite narrow in what it supports.
hiAndrewQuinn 13 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 15 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
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.
nextaccountic 22 minutes ago [-]
what's your language?
mejutoco 9 hours ago [-]
I dont think mathlib is mandatory to use lean.
empath75 8 hours ago [-]
It isn’t but the borrow checker has a formal proof that does need mathlib.
ndriscoll 7 hours ago [-]
You can define whatever you actually rely on as an axiom.
thaumasiotes 4 hours ago [-]
Publishing the proof is good, but why do you need it to build the language?
You can have one piece of software that does things, and a separate piece that proves that the things the first piece does are correct.
z0ltan 13 hours ago [-]
[dead]
Rendered at 22:28:25 GMT+0000 (Coordinated Universal Time) with Vercel.
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.
Kind of feels like you have to specify for what here, as no programming language is just "great at everything", they all have their places (except Clojure and children which is great at everything obviously). Say I run shell commands, obviously a PL based around proofs will be way too much, compared to if I want to create aircraft stabilizer with movable control surfaces.
However, after some consideration I opted to not move forward with it just yet. The problem is that at least for that particular case I could only really practically prove some properties of the code. With more time I could perhaps bring it up further. So for entirely practical reasons I am still going to want tests for the rest of the code. And while Idris 2 does have support for testing and continuous integration, at that time there were no solutions for measuring test coverage or performing mutation testing.
It does seem like since then someone has created a coverage tool for Idris 2, but mutation testing tooling still doesn't exist.
Lean 4 doesn't seem to have anything for coverage yet. I found some tool that claims to do a kind of mutation testing for Lean 4, but it sounds like it is still quite narrow in what it supports.
OTOH, my borrow checker is provably sound, which is why I am using it.
You can have one piece of software that does things, and a separate piece that proves that the things the first piece does are correct.