eyecode is a JavaScript rule language with forward and backward reasoning and checkable proofs. You write facts and rules in plain JavaScript; eyecode draws conclusions, and every conclusion can come with a proof that a separate checker verifies against your program. It runs as a command-line program, a JavaScript library, and a browser application, with no dependencies.
- Playground: run programs in your browser.
- Guide: run programs, write rules, check proofs, use the library, and develop eyecode.
- Specification: the language, its canonical text, the proof format, and the C1–C8 checks.
- Examples: 80 runnable programs, with their conclusions, proofs and check reports, and a card deck for each.
- Conformance suite: 353 cases that test any implementation of the specification through its command line.
fact(type('socrates', 'human'))
fact(subclass_of('human', 'mortal'))
implies([type(S, A), subclass_of(A, B)], type(S, B))
query(type(X, Y))
node bin/eyecode.js examples/socrates.js
node bin/eyecode.js --proof examples/socrates.js > /tmp/proof.js
node bin/eyecode.js --check-proof /tmp/proof.js examples/socrates.js
MIT licensed; see LICENSE.md.