Take a look at https://www.idris-lang.org/ https://www.idris-lang.org/ While I think it doesn’t check most of your boxes, it’s one of a kind in that it lets yo

Take a look at https://www.idris-lang.org/ https://www.idris-lang.org/ While I think it doesn’t check most of your boxes, it’s one of a kind in that it lets you write mathematical proofs for your functions. It pushes the limits of type driven development. As I understand, the big idea is that tests can only show a program is faulty, not that it’s correct. On the other hand mathematical proofs can actually prove your program is correct. That said I’ve never used it myself but I know a close-knit community of extremely smart mathematicians/programmers using it. It’s certainly a language with huge potential. I plan to play with it / learn it some day.