Synthetic Philosophy and Deductive Engineering
This is the top-level documentation for the administrative aspects of the SPaDE project. It falls into the following parts:
The SPaDE project begins as a github repository, which will eventually contain code implementing support for the representation of declarative knowledge in SPaDE repositories, for deductive reasoning in the context of that knowledge, and for solving both abstract and real world problems by deductive methods which give high levels of assurance moderated only by the fidelity of the scientific laws which underpin the abstract models. The project is intended to achieve efficiency in these applications by reflection, continuing once established to improve its own processes and structures through self-analysis and adaptation.
The intended role of reflection requires that the descriptions of the system which we use during its development become part of the declarative knowledge represented within SPaDE repositories.
SPaDE is intended to provide these services not directly to people, but to intelligent systems such as LLMs that interact with it using the MCP protocol and because the languages at present used in the development, which will include a great deal of English, HOL presented in a form suitable for human comprehension, and programming languages such as python also designed for the convenience of homo sapiens. If the development were conducted by non-human intelligent systems, there is little reason to believe that these languages would play the same central role, or that the considerations of human convenience would be as significant. It is already recognised by many, that as coding becomes entirely mediated by intelligent systems, the role of human-oriented languages and considerations of human convenience will be confined to those rare occasions when humans seek detailed technical information which would otherwise be inaccessible to them.
In order to effect the development of SPaDE (which is at present, and likely to remain, a single person project), extensive use of AI will be necessary and in order for large amounts of agentic work to fit together into a whole which meets the project’s objectives, careful coordination and adherence to well-defined protocols will be required.
In doing this, it is desirable that we continuously consider how the project documentation could be made fully formal and incorporated into SPaDE repositories, to enable the project to continue after the existing git repository is wholly migrated into the SPaDE repositories, bearing in mind that the role of human-oriented documentation will diminish as the project becomes increasingly mediated by intelligent systems. In devising and evolving the project structure and the manner in which that structure is documented, we must continuously consider how those structures might be formalised and maximise the extent to which their presentation is conducive to it. )
The project is organised into subsystems each with its own top-level directory. Some project activities, e.g. outreach are not oriented to the production of SPaDE subsystems but will neverthess get a directory for their work and associated document series. A top-level docs directory provides materials not specific to any single subsystem, which includes the important philosophical side to the project and materials relating to the overall architecture and design of the system as a whole.
In order to make clear the distinction between architectural matters and implementation detail, the division between the material in docs and that in the subsystem directories should be that architectural and philosophical content resides in docs, while implementation-specific content resides in the respective subsystem directories. That leaves unclear what the distinction is, and the answer to that is, that certain some interfaces are intended to be open to systems other than SPaDE, even when they provide functionality similar to components of SPaDE. Thus, and perhaps most crucially, the abstract structure of SPaDE repositories is architectural, but the way in which those structures are committed to permanent storage is not. SPaDE provides its own native representation for those abstract structures, and may also provide access to alternative stored forms, or provide SPaDE views over other kinds of knowledge or data storage, but it is open to any other provider to provide alternative stored forms or access to additional types of storage. This kind of distinction also applied to the concrete syntax associated with the formal specifications in SPaDE repositories. Concrete syntax not intended to be withing the scope of SPaDE, which is intended to deliver its services to LLMs or other intelligent systems using the MCP protocol. Any support for concrete syntax within SPaDE will be transitional. It is expected that metadata governing the presentation of specifications will be stored in spade repositories, but this is the responsibility of the agents using the SPaDE system, not of SPaDE itself.
The docs directory also has an admin subdirectory for materials of a non-technical nature, including project management and collaboration policies and procedures, and guidance for potential contributors.
Where there is no compelling reason to do otherwise, documents will be written in github markdown, and will be organised in such a way as to provide a transparent and complete view of the project from the project web site on rbjones.github.io/SPaDE Formal materials where appropriate may be presented in markdown as literate scripts.
The SPaDE documentation mostly falls into the following categories:
The general policy on naming of documents is that they should be in numerical series prefixed by short identifiers for the subsystem or subdirectory, and for the kind of document as follows. This seems to be morphing to using the subsystem codes for directories, whether or not they are subsystems, so that the README.doc indexes all the documents with the same subsystem code.
This needs to be made sufficiently systematic for all contributors (including copilot) to be able to choose filenames and maintain README.md files consistently.
Within each document-type group, README.md entries should normally be kept in numerical order by document number, with the lowest numbered document first. This is the default convention for admin, subsystem, and top-level documentation indexes because it makes browsing, diff review, and later automation easier. The numbering convention is therefore more than cosmetic: it provides a stable, predictable ordering that contributors and agents can rely on when scanning the project or adding new documents.
The current baseline does not need explicit marking in each README line item. When a document is active, list it normally. If a document is retained but retired from active use, mark it with strikethrough while preserving the live link. Keep the ordering numerical either way.
A README.md for a directory should list every document in that directory that still exists. An entry should be removed only when the underlying file is deleted. This preserves a complete index and makes it clear when project documentation is being kept intentionally, not merely forgotten.
When a document is retained for historical interest but is not part of the current working baseline, it should be marked with a strikethrough while keeping the link active, for example:
In Markdown, strikethrough is written as:
`~~[ampd001.md](/SPaDE/docs/admin/ampd001.html)~~`
and it can be applied to the linked label so that the link remains usable. This is the preferred concise indication that a document remains available for reference without implying current normative status.
Current procedure documents should describe enduring policy and working methods, not time-sensitive commentary about the state of tools, product changes, or temporary debates. Explanations of why a particular tool or workflow was being evaluated, or material that depends on a short-lived product state, belong in change histories, review reports, or chat logs rather than in the standards themselves.
In other words: the standard should record the endpoint, not the temporary path. The substantive content of a procedure should remain readable as a stable instruction, while the historical narrative belongs elsewhere.
Subsystem codes:
YYYYMMDD-HHMM-author-topic.md, see reviews.Document kinds:
After the two prefixes documents will have a three digit number starting at 001 for each kind of document. This completes the basename. Document name extensions will generally indicate the language in which the document is written, or the coding format. In some cases documents will have derivatives whose filename has the same basename but a distinct extension. This will happen when code or formal specifications are included alongside explanatory text in an .md file, or when the processing of one kind of formal text yields some other file (e.g. compiling a source module into an object module). Except in such cases of derivative documents, basenames should be unique. Derivative files having the same basename but a distinct extension should not be linked to separately in the README.md of the their directory.
Document headers should be avoided in markdown pages because of the impact on web page readability and presentation. A footer is more acceptable. Dates need not be included, history can be traced through git logs. The primary author should be indicated, which in the case of copilot should include the model name. Where a document results from conversation with an AI agent a link to the chat log should be included.
In the case of code or formal specifications not embedded in markdown a brief header mentioning authorship, including model name if AI.
This includes:
Guidance for potential and actual collaborators, both human and AI, either in this project or in associated but distinct enterprises,including:
admin/ (apart from one in the .github directory)admin/ directory and will be referred to in the relevant high-level documentsThere was previously an intention to use markdown more exclusively, as in a literate script system, including for formal specifications or code, and at that time the following exceptions were noted. The following exceptions to the policy were then noted, but probably are no longer relevant, insofar as there is no longer an intention to use markdown as a literate programming system.
There may be a small number of papers prepared as if for publication in the proceedings of conferences, in whatever the required format is (normally latex with a special formatting). Where possible these may be constructed using the markdown package to include markdown sources.
The retro/ directory is bootstrap, not SPaDE. It holds historical ProofPower literate scripts, mostly .pp files, so that ProofPower can be used while SPaDE cannot yet check its own specifications. It does not follow the documentation standards that apply in the other directories. ProofPower itself is transitional and is not a SPaDE deliverable. Formal specifications in HOL written for SPaDE and placed in markdown documents are part of SPaDE.
It is likely that a compendium of project documentation as a PDF reference manual will be desirable if the development is successful. This would likely be produced by texlive, mainly compounded from .md files incorporated using the markdown package or converted to .tex files using pandoc, with one or more .tex files glueing them together.
In SPaDE proper, during the bootstrap process, §HOL is written in markdown. The method is amms012.md. docs/tlci001.mkf strips the formal text and loads it with ProofPower.
Eventually, the specifications, and the entire project, will migrate into SPaDE repositories (not the github spade repo).
A document derived from a ProofPower source, or from another document in the repository, acknowledges that source. A specification opens a theory with new_SPaDE_theory, defined in tlcd002.md. A theory name is brief and suggestive of the nature or role of the theory. Correspondence with the document name is not required. The makefile records which document creates which theory by making the theory listing depend on that document’s load. The procedure is in ampd012.md.
It is policy to progress all informal documentation into formal models at all levels. They will then migrate into SPaDE native repositories. At the lower levels this is part of the reflexive reasoning required to approach the first singular foci and is therefore of high priority. At the higher levels it is probably less urgent.
The reflexive nature of the project architecture means that from the earliest possible stage the abstract representation of algorithms will be in the HOL abstract syntax, and concrete syntax will be supplied as required by LLM like general intelligence in an outer shell. The implications of this for the documentation is not yet clear, but the preference will continue to be to address the needs through descriptions in github markdown documents. First prototyping of the logical kernel are likely to be by transcription from HOL to SML.
When undertaking reviews, please place outputs from the review in a markdown file in the “reviews” directory file in the root of the repository, or in a subdirectory of that directory if the comments relate to a specific subproject. Use a filename which includes the date and time of the review followed by the contributor name, (e.g. copilot). The date and time should be rendered in a formal which collates the files in temporal order in a directory listing, e.g. 20241001-1530-copilot.md for a review made on 1st October 2024 at 15:30 by copilot. A further component of the filename may be a brief indication of the subject matter, e.g. 20241001-1530-copilot-KRreview.md Avoid using colons (:) in filenames as they cause issues with Jekyll/GitHub Pages processing.
This policy will evolve as the project develops and we learn what works best for our collaboration and documentation needs. All changes should be documented and justified based on our experience.