I've been interested in this question myself - and recently wrote a basic web 'microframework' for Lean 4 [1]. I've loved being able to use Lean's macro system

I've been interested in this question myself - and recently wrote a basic web 'microframework' for Lean 4 [1]. I've loved being able to use Lean's macro system to write JSX-like HTML: def header := <header class_="header"> <h1>todo</h1> ... Ironically I've come up a bit short on how to use dependent types to do anything more advanced than matching handlers' to route types, which Servant [2] can do fantastically already. I would love to be able to write types that describe, e.g., assumptions made about external resources, so that I can prove that "assuming my DB has such-and-such a latency, my page will always render in such-and-such a time" or something similar - but it's a bit beyond me at the moment. [1] https://github.com/alex-wellbelove/LeanServer https://github.com/alex-wellbelove/LeanServer [2] https://hackage.haskell.org/package/servant https://hackage.haskell.org/package/servant