From a752bf644497fc905e87897d704b410990c30e36 Mon Sep 17 00:00:00 2001 From: Timothy Pratley Date: Mon, 12 Dec 2022 13:16:50 -0800 Subject: [PATCH] Improves README.me with more information These updates are based upon the Lisp In Small Peices bookclub meeting held on dec 10 during which Chris presented Halite to the group. Unfortunately the current "overview" documentation link is dead. I tried running the `(generate-local-docs)` task, but it fails due to missing files. If you have the files, please consider adding them to the repo so that the overview can be generated. --- README.md | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 55 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 5d23224c..cc5de4d7 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,59 @@ # Halite -The successor to [Salt](https://github.com/Viasat/salt). +A tool for specification and verification of systems. -[Halite Documentation](doc/halite_outline.md) +Halite consists of -Please note this is a pre-release version and the API is unstable. +1. A specification language for defining schemas and constraints +2. An evaluator that can be used to verify instances or compositions of schemas and constraints. +3. A generator that can create possible solutions. + +Halite is the mineral form of salt (sodium chloride) commonly known as "rock salt". +This tool is named Halite as the successor to [Salt](https://github.com/Viasat/salt) +(S-expressions for Actions with Logic Temporal). +Salt provided a Clojure interface to TLA+. +Halite provides Edn and Json interfaces for specifying schemas +and constraints. Constraints are solved by [Choco-solver](https://choco-solver.org/). + +## Rationale + +Systems are composed of services. +Service components are often maintained by different teams. +The interfaces and behaviors of the system need to be clear, precise, and verifiable in order to create a cohesive system. +Halite provides a formal way to define interfaces and behaviors. +Using this approach to model and reason about a system enables proof that the design is logical, and that the outcomes are known. + +We see potential use cases to include + +1. **Proving systems.** As a standalone proof system to ensure that the designed composition of services is logical, and that specific instances of communication are valid. +2. **Constructing systems.** As an integrated shell for the system that automatically validates boundary communication. +3. **Applying constraints in programs.** Integrated into services to validate inputs and outputs of processes. + +## Usage + +This is a pre-release version and the API is unstable. +No releases are available yet, instead clone this repo or use as a git dependency. + +## Documentation + +Coming soon: [Outline](doc/halite_outline.md) + +Meanwhile: + +* [Fields](doc/halite/explanation/halite_abstract-field.md) +* [Specifications](doc/halite/explanation/halite_abstract-spec.md) + + +## Contributing + +Pull requests and issues are welcome. + +### Setup + +Install Leinigen and Java. + +### Testing + +``` +lein test +```