alt Hacker News> obviously no one’s running any compiled Lean code in any kind of production hot path
Ignorant question: why not? Is there an unacceptable performance penalty? And what's the recommended way in that case to make use of proven Lean code in production that keeps the same guarantees?
Yes, it isn’t performant. Lean isn’t a language for writing software, though you technically can; it’s a language for proving math.