Skip to content

Improves README.me with more information #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
timothypratley wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Improves README.me with more information #1

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 55 additions & 3 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
```