Hacker News Reader

Are you programming in Fortran?

That's a bad analogy. LEAN is a leading bleeding edge proof verification tool.

Fortran used to be the only programming language (and even cutting edge by default). People went off and created new ones anyway.

And maybe somebody will create something better than LEAN. That has nothing to do with the original argument.