Certificates

Clients can create and modify ordinary object content pretty much free form. But they cannot force a certificate with a certain content to be created or altered or, when objects referenced by a certificate are altered, to be preserved; certificates are a kind of derived content. The client can delete them, with consequences, and request certification services such as attempting to create certificates of specified kinds. The client can also create content that refers to certificates, just like to any other objects. See Current Closed Maps.

Certification services and kinds of certificates are open-ended, subject to extension by implementation. The basic significance of each kind of certificate must be explained when it is introduced, and provides a basis for promises and correctness claims on the part of the system implementors. See Certificate Significance and Certificate Structure.

The dominant kinds of certificates we have been anticipating are for formal proof certification, recording claims that certain inferences have been validated via specified methods.
The basic intention we anticipate is that a kind of certificate is designed with the aim of supporting claims about closed maps based upon the existence and content of those certificates.
Here is a strong paradigm case: the client may infer from a certificate about a formal proof that it conforms to specific methods of inference, and could test this claim.

Consider also an example of a form of certificate which has no value, its being simply an extreme possibility: suppose that a certain kind of certificate can be created willy-nilly by the system and added to the client's current closed map, and that it has no content except the indication of its kind; there is nothing of interest that one may infer from the existence of such a certificate.

Another kind of certificate that would be useful: the client may ask that a certain compiler be run on some source code object in the current closed map; the system then runs the compiler according to the specification, saves the output as a new object in the current closed map, and adds a certificate of this kind that points to the source-code object as well as to the new load-module object (say); if one later wanted to execute the code, one might use the existence of this compilation certificate to justify later claims about execution of this program involving the load-module.

Another: a certificate kind could be designed to mean that, by some specified method, a date and client identity for a Session have been ascertained when a certain object has been updated or created.

In each of these scenarios it is possible for multiple certificates of various content and import to be created by the system. Thus, a Proof or Inference Step might be validated by several independent (in various ways) Inference Engines, each certified; different compilers might be applied to the same source code, the certificates indicating them and their outputs; different means of establishing date and identity might be employed, with perhaps with varying degrees of credibility.

We give preferred treatment, described in Certificate Bias, to certifications of facts about closed maps that are abstract, monotonic, and "localized". IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html