Sooner or later software breaks

The world is becoming more and more dependent on software, still society lacks a reasonable way of creating dependable software. A lot of research time and effort has been spent on the ways to prove correctness (free of bugs). Broadly speaking there are two approaches: Theorem proving and Model checking.

Both methods are far from being mainstream and are usually applied only in very specialized situations by academics when correctness is of utmost importance and bugs are very costly. We have made it our mission to continue this research and make software correctness attainable for everyone.

Theorem proving

Theorem proving is used to prove the correctness of the se4L micro kernel. Concurrent or distributed programs, such as (micro kernel) operating systems are notoriously complex, and thus offer an excellent area of research.

See se4L as an example of why correctness is important.

What is theorem proving?

It is a method to verify procedure by procedure, whereby for a given precondition the corresponding postcondition is met through symbolic execution with the help of a proof assistant.

This approach offers freedom with respect to which properties are to be proven, as well as the level of fidelity of how accurately the model represents the program at the cost of manual effort and expertise.

Model checking

Another approach to formal verification is model checking. The Reasonable Sourcery founders have been working collectively in a commercial setting for 30 years to create a programming language with builtin model checking: Dezyne.

By creating Dezyne we demonstrated that engineers in an enterprise setting are successful and effective in adopting and applying formal methods in their product development, see:

@ThermoFisher Scientific Electron Microscopes.
@Philips Healthcare Image Guided Therapy.
@ASML Litography Systems.

What is model checking?

In model checking you describe an abstract version of your program and use a model checker to automatically verify a given set of properties.

The process of model checking is similar to testing. The difference being that it is fully automated, exhaustive and far more efficient.

|                 | advantages   | limitations                            |
|-----------------|--------------|----------------------------------------|
| theorem proving | any property | only by experts                        |
|                 | any size     | labor intensive                        |
|-----------------|--------------|----------------------------------------|
| model checking  | automatic    | properties expressed in specific logic |
|                 |              | verification computationally bound     |

Dezyne employs compositional verification to allow scaling model checking for large systems and industrial use.

Currently, Dezyne verifies the absence of non-determinism, deadlock, livelock, undesired behavior, unreachable code, invariant violation, and non-compliance between interfaces and implementation. We aim to further extend this list of properties and the expressiveness of the language.

See mCRL2 for the logic of properties and models underlying Dezyne and the solution to pushing the envelope on the limitations of model checking.

Reasonable Sourcery ultimately aims to augment Scheme through a SRFI

Dezyne's success has convinced us that model checking is a more than promising direction; it must become ubiquitous. Although Dezyne itself is entirely written in Guile Scheme it targets a very specific niche: machine control, catering for corporate adoption; a C-like programming language that targets C++ users.

The main reason we have founded Reasonable Sourcery is to create a sociocratic research and development worker cooperative to widen the niche and bring model checking to the Free Software community as simple and elegantly as possible. We will start by extending Guile and aim for standardization as a SRFI.

For starters, we will apply this in order of appearance in:

GNU Shepherd herding system and user services in Scheme.
Spritely Goblins next generation of decentralized networking technology.
GNU Hurd micro kernel with hird of unix of replacing daemons.

such that formal properties and models can be specified and extracted for automatical verification of these projects.

Vision