I am announcing Minuska: a truly formal programming language framework. One can use Minuska to specify programming language semantics - formally. From the semantics, Minuska can automatically derive a formally proven interpreter for the language. Minuska is formally specified, implemented, and proved using the Coq theorem prover, with a bit of OCaml used for its command-line interface.
Minuska is my academic attempt to address some of the limitations of programming language frameworks that I mentioned in my previous posts: namely, that frameworks like PLT-Redex and K do not have formal semantics themselves, and thus one cannot precisely reason about languages defined in and tools written for these. Minuska can already handle a simple imperative language and generate a reasonably performant 1 interpreter for it.
Minuska is still a research prototype rather than a mature tool: it does not come with comprehensive documentation and the syntax of its input language is subject to change. Moreover, Minuska is only a semantics framework, and does not deal with concrete syntax of programming languages: users are expected to write their own parsers for their languages. Therefore, users in a serious need of a programming language framework are advised to have a look at K or PLT-Redex.
That said, I invite anyone interested to play with Minuska, open issues, create pull requests, and offer suggestions for future work (some of which is described in doc/ideas.md).
Minuska is available on GitHub under MIT license:
https://github.com/h0nzZik/minuska
-
slow, but not that slow ↩︎