you are viewing a single comment's thread
view the rest of the comments
[–] 4 points 1 year ago (1 child)

I hadn't seen Idris2. Thank you for providing me with a new rabbit hole!

  • source
  • parent
  • hideshow 1 child comment
  • [–] 3 points 1 year ago

    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.

  • source
  • parent