Cypher1 / tako

An experimental programming language for ergonomic software verification
https://takolang.dev
MIT License
15 stars 1 forks source link
experimental-programming-language hoare-triples interpreter language programming-language-theory solver verification

Tako

All Contributors

Cherry Build Status GitHub issues

An experimental programming language for ergonomic software verification using Hoare Logic.

Getting Started

These instructions will get you a copy of the project up and running on your local machine for development and testing purposes. See deployment for notes on how to deploy the project on a live system.

Prerequisites

Tako currently uses cargo for builds and running tests and git submodules for dependency management.

Installation instructions can be found at https://rustup.rs/

Building

Building is a single step,

cargo build --release

You can also install tako, though I don't recommend this.

cargo install --path=./tako

This allows us to run the compiler.

tako examples/hello_name.tk
./build/examples_hello_name 'world'

And interactive interpreter:

tako -i

And use the interpreter to run a tako file:

tako -r examples/hello_name.tk -- 'world'

Running the tests

Running the tests is also a single step.

cargo test

Note: Currently this tests using an optimised build as some of the tests rely on rust optimisations that decrease stack usage. Tracking bug: https://github.com/Cypher1/tako/issues/179

Installation

Warning: Don't use tako. Use some other language & compiler.

I recommend rust, haskell or idris.

tako is not stable, reliable, or efficient.

You have been warned.

tako is a standalone single file. It can be installed simply by building and copy/moving ./tako into your /usr/bin directory.

Contributing

Please read the CODE_OF_CONDUCT.md and CONTRIBUTING.md guides for details on our code of conduct, and the process for submitting pull requests.

Versioning

We will use SemVer for versioning. There are no versions currently available, but see the tags on this repository.

License

This project is licensed under the MIT License - see the LICENSE.md file for details

Acknowledgments

Contributors

Jay Pratt
Jay Pratt

💻 🎨