Website contains:

• Development blogs which are written for general audience
• Installation instructions (basically telling you what to download in GitHub Releases)
• Tutorial for functional programming features
• Tutorial for theorem proving features

Warning

Aya is under active development, so don't be surprised about bugs, usability or performance issues (please file issues or create threads in discussions!), but we have the goal to make it as user-friendly as we can feasibly do.

What to expect?

It might be concerning to a lot of people that Aya is written in Java, because a common misconception is that whatever written in Java will be (1) use loads of bloated dependencies and (2) require a Java runtime installed separately. Neither of them are true: (1) Aya codebase is very small, and we rely on as little external dependencies as possible, (2) Aya releases are self-contained and are designed to run on Java-free environments (see GitHub Releases).

• Dependent types, including Π-types, Σ-types, indexed families, etc. You could write a sized-vector type.
• Set-level cubical type theory (XTT).
  • Demonstration of quotient-inductive-inductive types, no forward declaration or mutual block needed! We infer the type checking order by how definitions use each other.
  • Proof of funExt in paths.aya.
• Pattern matching with first-match semantics. Checkout the red-black tree (without deletion yet).
• A JIT-compiler that translates Aya code to higher-order abstract syntax in Java. This makes the interpreter to run tree-sort 10x faster! See benchmark code.
• Overlapping and order-independent patterns. Very useful in theorem proving.
• A literate programming mode with inline code fragment support, inspired from Agda and 1lab. You may preview the features (in Chinese) here.
• Binary operators, with precedence specified by a partial ordering (instead of a number like in Haskell or Agda).
• A fairly good termination checker. We adapted some code from Agda's implementation to accept more definitions such as the testSwapAdd example in this file (which are rejected by, e.g. Arend).

See also use as a library.

TODO and Under Development

• A class system similar to Arend, used to organize mathematical structures and proofs.
• Positivity checking for higher inductive types.
• I want to completely rework the VSCode extension. Right now, it just doesn't load. I also lost access to my VSCode marketplace email.
• Something similar to rustup but for Aya.

Contributing to Aya

See HACKING.md for technical details, CONTRIBUTING.md for social responsibilities, and CODE_OF_CONDUCT.md.

Questions are always welcomed in Discussion. We will try our best to answer your questions. Please be nice to us! We also welcome nitpicks on any user-interaction issues, especially on error reporting. Let us know if you have any suggestions.

Use as a library

It's indexed in mvnrepository, and here are some example build configurations:

<!-- Maven -->
<dependency>
    <groupId>org.aya-prover</groupId>
    <artifactId>[project name]</artifactId>
    <version>[latest version]</version>
</dependency>

// Gradle
implementation group: 'org.aya-prover', name: '[project name]', version: '[latest version]'

• [project name] specifies the subproject of Aya you want to use, and the options are pretty, base, cli-impl, parser, etc.
  • For the list of the subprojects, see HACKING.md.
• [latest version] is what you see on this badge .