ideas.md

Minusa - ideas and missing features

Concrete syntax of programming languages

Minuska operates on an abstract representation of programming language syntax. There is currently no support for specifying, parsing of, and unparsing into concrete syntax of programming languages.

Semantics of contexts

Currently, strictness declarations and contexts are implemented by desugaring them to rewriting rules by the frontend. While this approach works, it does not equip the user with any means of high-level reasoning about the high-level constructs (that is, contexts and strictness). We are working on a precise syntax and semantics for contexts, with an explicit translation to rewriting rules that should be formally verified to preserve the semantics.

Symbolic execution

In principle, it should be possible to generate symbolic execution engines for languages defined in Minuska, simply by using unification instead of pattern matching in the interpreter. An option would be to use the Coq Color library which already contains a provably correct implementation of an unification algorithm. However, this has not been implemented yet. Even if this gets implemented, we would need to have a simplification engine to prune infeasible branches; this would be best done using some LTac scripting inside Coq, using tactics like lia, itauto, and possibly smt.

Deductive verification

K Framework a implements coinduction-based logic (reachability logic 1 2) that can be used to prove partial correctness properties of programs with loops, recursion, or other source of circular behavior. This would be nice to have, but it depends on the symbolic execution being implemented.

Testing type soundness

We could use the QuickChick framework to automatically test whether a given language definition behaves reasonably on well-typed programs. This includes the absence of calls to builtin functions that would return an error value.

Fast rule selection

We can do better than linear search for selecting a rewriting rule. There is the paper Compiling pattern matching to good decision trees which we should implement. The diffference here is that our rules have side conditions, and therefore we need to choose all suitable rules, not just a one - what if the side condition of the selected rule does not hold? There is a WIP implementation in dt.v.