Software Foundations being translated to Lean (leanprover.zulipchat.com)

I was just looking into this. Found https://github.com/PnVDiscord/software-foundations-lean and some other chatter about the concept, but it wasn't active, lots of sorry in the basic library etc.

Oh it's by Benjamin Pierce's team too that inspires much more confidence lol. Ready in fall I'll set a reminder, exciting stuff.

I guess this means the whole space is settling around lean? (at least for capital A Academia and Industry)