[hirple]

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 [2] https://hackage.haskell.org/package/servant

[ykonstant]

Before taking the plunge on using dependent types in production, please heed the warnings discussed here: https://lean-lang.org/functional_programming_in_lean/depende...