Racial justice, social justice, environmental justice—all good causes seem to be justice nowadays. Everything is a struggle between the condemned and the enforcers. Either you are an oppressor or you are one of the oppressed.
Is this a healthy way of looking at the world?
Now targeting JDK 19 for preview.
SWIFT is really just a glorified instant messenger. Money movement works without it, just less conveniently.
A tutorial on Z3. Z3 is a SAT solver. It is used as the underlying deduction engine in many applications that need a theorem prover.
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.