An imperative language with a verification calculus built in.
Low* is a language embedded in F* that can be used as an alternative to C for low-level programming, but inherits F*’s proof and verification capabilities. By using Low* you can write low-level code and prove it correct, all in one language.
KaraMeL (née KreMLin) is the Low* compiler.
There is a research branch of Scala 3 that contains a feature called Capture Checking. Capture Checking is a way to track effects in a way that works well in imperative code.
Instead of relying on monadic composition the way other contemporary functional languages do, Scala 3 annotates variable types with capability sets, which define what effects and objects a value is allowed to access. It seems to be inspired by Borrow Checking in Rust and looks very similar.
I’ve long found it somewhat ironic that Scala was less safe than Java because it did away with checked exceptions. This finally gives it checked exceptions back.
A static checker for specifications written in the Java Modeling Language. Only supports a subset of Java 7.
A design-by-contract and model checking specification language for Java.
Put a REUSE comment in the top of each file:
SPDX-FileCopyrightText: © 2022 Jane Doe <jane.doe@example.com>
SPDX-License-Identifier: AGPL-3.0-or-later
This way your licensing information is unambiguous and machine-readable.
The University of Helsinki’s introductory programming course. Unabridged and of fair repute. No prior programming knowledge required.
A GHC type checker plugin that enables you to specify rewrite rules in order to prove type equalities.
Has a nice list of alternatives in the bottom, too. Among them:
- ghc-typelits-natnormalize, a GHC plug-in
- Thoralf, another GHC plugin
- Liquid Haskell
- Ghosts of Departed Proofs, a library
- an approach called Hasochism
GitHub’s Rust implementation of stack graphs.