The model of distribution
The validity of a mathematical document A that
refers to a document B can be guaranteed only if B does not change
===> mathematical documents should be immutable
Conjectures could be prooved, theories could be
augmented ===> new versions of a document could be released
We cannot force users to maintain forever the
documents they have written (and in the same place) ===>
need for logical names (URIs) instead of phisical names (URLs)
(e.g. "cic:/coq/INIT/Datatypes/nat.ind")
Many copies of a document could exist, provided by
different servers (HTTP, FTP, ...) ===> we need "getters"
that, given an URI and an (ordered) list of servers, return the
instance of the document provided by the nearest (first) server