alt Hacker Newsdon't disbelieve you, but just looked at the reference language, it seems pretty full featured as a programming language, even with basic classes, polymorphism, scope, namespaces... But maybe most of the mathematicians who actual code with stick with the simpler language features? And also, didn't look to deeply, these could be very simple features that actually aren't very sophisticated.
I mean Lean has two things: a full programming language, and proof checker. The programming language is used to create either code, or proofs. But the "created proofs" are using a very simple subset (a bit like an "assembly language"), and only need somewhat simple rules to be checked
So as long as the "somewhat simple" core that checks to proof is correct, it doesn't matter if the "programming language" has bugs: either in the end the "proof assembly code" generated by the program is right and is validated by the core, or it's not, and you need to revise your proof, or to check for either a bug in the programming language (it didn't generate the proof you were expecting), or in very rare case detect a bug in the simple "core"