i feel like this would be the equivalent of having all CS undergrads program with assembly and assembly only.
it might(?) work? but abstractions exist for a reason (mostly...)
Once upon a time this was all there was, so it naturally was proven to work as it was easier than dealing with boards full of dip switches that predated them.
Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be.
It's completely different things. Math itself is abstraction. Lean is formalized abstraction that don't let you write "it is immediately obvious that"