The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

[decloaking from lurker mode to add my $0.02]

Does having LEM built into Lean interfere with the user's ability to exploit 
the Curry-Howard isomorphism?

If so, that seems like a bad trade off: a small convenience for a
small group of people (Fields Medal wanabees) that imposes a large
inconvenience for a large group of people (software engineers).

Which is not a problem if the choice remains Coq for software (et. al.),
Lean for math (pure as the fallen snow).  It might become a problem if
an insistence that Lean's way is the best way depleted that choice.

I am also reminded of a possibly (in)appropriate quote attributed
to a product marketing exec at a defunct software company I worked for
many years ago: "I would like to decrease the IQ of our customer base by
25%".  If we had only managed to pull that off, we'd still be in
business.

Seems like Lean may be leaning the other way.

[recloaking...]