Slang is a modern mix of object-oriented/functional programming language with contract and proof languages designed first for formal safety/security verification and analyses. It serves as the basis for the Sireum Logika verification framework, as well as for other formal method-based analysis techniques. Some key Slang designs to ease program reasoning are: (1) explicit separation of immutable and mutable static types, where immutables cannot refer to mutables, (2) object aliasing is restricted to a single language construct, i.e., method invocation, which has an intuitive and natural object borrowing boundary scope for compositional reasoning, and (3) a forest of type hierarchies (instead of a single rooted tree) for a more meaningful subtyping relationships.
Slang is currently a subset of Scala 2 with tailored semantics
enabled via Scala’s macro and compiler plugin facilities,
supported with a customized version of IntelliJ –
Sireum IVE, and an accompanying
incremental/parallel build tool – Proyek.
Most of the Sireum codebase is written using
Slang (including Slang itself).
Slang programs run on the JVM (Java 8+), in the browser or Node.js
via Graal targeting macOS, Linux, and Windows on amd64, and
macOS and Linux on aarch64.
In addition, the Slang-to-C transpiler
can compile a subset of Slang – Slang Embedded
to C without garbage-collection at runtime.
The generated C code is both Slang source-traceable and
in the form that is structurally close to the Slang source;
in addition to
clang, it can also be compiled using the
CompCert Verified C Compiler
to provide a high-assurance toolchain for program correctness down to machine code.