The Coq mailing list

[Andrew Appel <appel AT princeton.edu>]

+1

---

From: "Ralf Jung" <jung AT mpi-sws.org>
To: "coq-club" <coq-club AT inria.fr>, "Guillaume Melquiond" <guillaume.melquiond AT inria.fr>
Sent: Friday, September 18, 2020 10:46:09 AM
Subject: Re: [Coq-Club] option to disable partially qualified Require Imports

Seriously though, I do not understand this attitude.  No other language that I
know of has a module system as strange as Coq's (maybe this is inherited from
OCaml?), and yet you claim that it's the library author's fault for not taking
care in designing their library to work around this quirk, rather than the
language designer's fault for having designed something strange.  (Probably the
language designer had a good reason and this was solving a concrete problem, but
putting the blame on the library is just unfair. And you haven't argued for why
Coq's semantics make any sense, either.)

This is not about malicious users, it is about people coming to Coq with what I
consider reasonable expectations having their code break for reasons that are
really hard to figure because Coq violates assumptions formed when learning
pretty much any other language. Even the notoriously sloppy _javascript_ requires
precise imports! I still remember my surprise when I learned about "-R"
semantics... it remains a mystery to me how it seemed like a good idea to just
recursively slap everything into the global namespace. And then when "From ...
Require" was introduced I was very surprised to learn about its path matching
semantics, I had not even realized that regular "Require" was not doing
full-path matching either. For what is otherwise a system that is extremely
picky about which terms it accepts (for good reasons!), this stands out like a
sore thumb.

There probably is a reasonable explanation for this. But dismissing the concern
as only affecting "dumb" users is not reasonable.

Kind regards,
Ralf