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.
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
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.
> 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.
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.
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.
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
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.
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.
OTOH, my borrow checker is provably sound, which is why I am using it.