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.
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.