News for hackers. Stuff that matters.

A comment on Abusing the algebra of algebraic data types – why does this work?. Parent comment

Re:Abusing the algebra of algebraic data types – why does th... by nequo on Monday October 10, 2022 @03:16PM (#33155359)
Lean 4 seems promising, too.[1] Although it looks very much like Haskell.

[1] https://leanprover.github.io/functional_programming_in_lean/

[ Parent | on HN ]
Re:Abusing the algebra of algebraic data types – why does th... by klyrs on Monday October 10, 2022 @03:20PM (#33155398)
Yes, progress is under way! It's been a few years since I tried to plumb these depths, it's probably time to look again. But I don't need to look to know that we're not there, where "there" means both accessible and widely adopted.
[ Parent | on HN ]
Re:Abusing the algebra of algebraic data types – why does th... by chalst on Monday October 10, 2022 @04:27PM (#33156039)
Lean is particularly exciting because of the work Kevin Buzzard has been doing in the Xena project:

https://www.ma.imperial.ac.uk/~buzzard/xena/

He started by getting undergraduates to tackle formalising the maths they did in Lean, and his success with this as a didactic tool has spread the idea among quite a lot if mathematicians.

[ Parent | on HN ]