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. Read more…