Very cool, I think Lean has incredible power as a declarative config language that hasn't been realized yet. I've been exploring how to use it for system configuration ala Nix

Thank you, yes, absolutely, and it's also the perfect language for an AI agents. The more refined the type system, the tighter the feedback loop for the agent.