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

• There is also the orthogonal naming problem ===> need for a naming authority or a more distributed solution