I’m glad to tell more people about it. It’s really quite amazing (I could write a somewhat complex algorithm and prove some properties about it in a couple afternoons, despite limited formal verification experience) and I’m sure that in 20 odd years the ideas behind it will make it into mainstream languages, just as with ML/Haskell.
You kid, but Idris2 documentation literally proposes almost this exact impl: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#note-declaration-order-and-mutual-blocks (it’s a bit facetious, of course, but still will work! the actual impl in the language is a lot more boring: https://github.com/idris-lang/Idris2/blob/main/libs/base/Data/Integral.idr)
I hadn’t seen Idris2. Thank you for providing me with a new rabbit hole!
I’m glad to tell more people about it. It’s really quite amazing (I could write a somewhat complex algorithm and prove some properties about it in a couple afternoons, despite limited formal verification experience) and I’m sure that in 20 odd years the ideas behind it will make it into mainstream languages, just as with ML/Haskell.