News for hackers. Stuff that matters.

A comment on Show HN: IHP v1.0 (Batteries-included web framework built on Haskell and Nix). Parent comment

Re:Show HN: IHP v1.0 (Batteries-included web framework built... by nequo on Monday October 24, 2022 @11:38PM (#33325894)
> There are plugins for Haskell and dependently typed languages that go much further in the ‘if it compiles, it is formally validated’

Yes, Lean 4[1] is shaping up to be a Haskell-inspired dependently typed language with monadic IO etc. that can also prove theorems for you. Still a work in progress but looks very exciting.

[1] https://leanprover.github.io/lean4/doc/

[ Parent | on HN ]
Re:Show HN: IHP v1.0 (Batteries-included web framework built... by epgui on Tuesday October 25, 2022 @12:14AM (#33326151)
See also:

- Idris (https://www.idris-lang.org/)

- Agda (https://wiki.portal.chalmers.se/agda/Main/HomePage)

I'm really excited by progress in this space! :)

[ Parent | on HN ]