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 Scala.js Javascript translation), and natively 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 gcc and 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.

On all compilation targets (e.g., JVM, Javascript, C, etc.), Slang provides extension method facilities that can extend its language features and integrate with other programming languages, platform-specific libraries, and existing/legacy code. Furthermore, Slang can also be used as a universal shell scripting language – Slash, which can run on macOS, Linux, Windows, and others where a JVM runtime is available. Sireum IVE supports Slash scripting. Slash powers many of the shell scripts for developing Sireum itself. As Slash is Slang, Slash scripts can be compiled to native via Graal, which speeds things up by virtue of having no JVM boot up time.