Repository files navigation

A programming language for verified software.

Type in the workspace directory:

cargo run nacre::std::logic::Eq::symmetric

This will verifyEq::symmetric in./nacre/std/logic.na.To verify any theorem of yours, type it in a fileand access its path like this. You can import symbolsfromstd using the following syntax:

usesuper::nacre::std::logic::Eq;

To useannotate-snippets for error reportinginstead ofariadne (the default), pass the--features annotate-snippets and--no-default-featuresflags tocargo.

At the moment, code generation is verybasic and the ABI is not complete.There is an integration test for compilation,which emits an object file and links itagainst a test program, which is then run.

cargo check# buildcargo clippy# lintercargotest# integration testscargo llvm-cov# test coveragecargo bench# performance regressionscargo mutants --test-workspacetrue# mutation testing

cargo afl build --example fuzz_consistencycargo afl fuzz -i nacre_kernel/examples/in -o nacre_kernel/examples/out target/debug/examples/fuzz_consistency

Currently, a compiler is being developed in Rust,but the roadmap is focused on eventual self-hosting.This means that this initial development will focusoncorrectness andcore features, but notnecessarily performance or even code quality(although readable code is desired, so as to serveas reference for later development).

• Complete and stabilize code generation.
  • Structs and enum variants with contents.
  • Built-in operators.
  • Array and integer types.
  • Generic types (and related CoC-level transformations).
  • Partial application.
  • Non-de-closureable usages.
• Finish core syntax.
  • Implement named parameters in function application.
  • Implement struct and enum definition syntax.
  • Add support for more kinds of lvalues.
  • Add core operators.
• Add tests.
  • Parser fuzz test.
  • Regular test suite.
  • Mutation testing.

Once the bootstrapping compiler is capable ofgenerating actual (albeit slow) code, the nextstep would be to carefully expand its capabilitiesand the standard library, working towards theimplementation of a self-hosting compiler.

• Implement macros.
  • Design the macro system.
  • Get JIT compilation ready.
  • Get basic macros to a working state.
• Improve logical foundation.
  • Allow axioms from allowlisted paths.
  • Explore if a generalized induction axiom can beexpressed and used in a reasonable way.
  • Explore whether axiomatization of type-specificindefinite description is consistent and sufficientto prove the types' uniqueness.
  • Investigate what types should be given thisaxiomatization at minimum (e.g. equality).
  • Write axioms.
• Extend the standard library.
• Implement low-hanging optimizations.

Having brought the compiler and language toa reasonable degree of maturity, the most criticaltask begins: writing a self-hosting compilerwith all the desired features, performanceand optimization capabilities.