Typesetting pseudocode

Stream: general

[Trebor Huang]

I would like to use some of the Lean/Agda/Coq-like syntax in LaTeX, mixed with mathematical notation. An example of what I want to achieve, done by hand.
typesetting excerpt
Is it feasible to write something that does this semi-automatically? Perhaps a code-generator plus a LaTeX package?

[Trebor Huang]

If there is previous work like this I would like to see if I can fit it to my needs. And if not, is it worth writing my own tools? Would somebody else want to use that?