The C# Multiverse — the Singularity of Programming Languages

8 min readMar 3, 2023

I started my acquaintance with .NET and C# in around 2007. At that time, I was studying in my fourth year and already had experience working with programming languages such as C++ and Delphi. Moreover, I even had a commercial product written in Visual C++ that worked quite well. However, even then, I felt constrained by the limitations imposed by Delphi and C++, so I started looking for alternatives. I worked a bit with different languages and technologies, and when I finally got to C#, I immediately realized that it was the tool that ultimately matched my requirements and was comfortable and convenient for work. Since then, I have been actively following everything that happens with the .NET platform and the C# language. At least, that’s what I thought until recently when I found few publications that introduced me to a few “parallel realities” where everything seems to be the same as here but slightly different. And I suggest to explore a bit more closely these alternative realities.

We must go back in time for about twenty years. In 2003 [1], in the depths of Microsoft Research (the research division of Microsoft Corporation, almost a secret laboratory), the work began on the Singularity project — a highly reliable operating system in which the microkernel, device drivers, and applications are written in managed code.

In their article “Singularity: Rethinking the Software Stack,” Microsoft Research employees James Larus and Galen Hunt describe Singularity as follows [2]: “In the Singularity project, we have built a new operating system, a new programming language, and new software verification tools. The Singularity operating system incorporates a new software architecture based on software isolation of processes. Our programming language, Sing#, is an extension of C# that provides verifiable, first-class support for OS communication primitives as well as strong support for systems programming and code factoring.”

The history of creating the Singularity operating system is fascinating and deserves a separate article. But the phrase “our Sing# programming language” caught my attention in this case. I had never heard of this programming language before and was interested in learning more about it. Unfortunately, the Wikipedia article [3] about Sing# was very short and presented in only two language versions — Russian and German. But despite the small amount of information, I found something else interesting there — the language description card indicated that the Sing# language was influenced by another language — Spec#, it means that we already have two related C# programming languages.

Since Spec# is the basis for Sing#, I started looking for more detailed information about it. Microsoft Research describes this language as follows [4]: “Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants.”

Regarding Sing#, the publication “An Overview of the Singularity Project” said that [5] “Sing# is an extension of C# that provides verifiable, first-class support for OS communication primitives and strong support for systems programming and code factoring. The sound verification tools detect programmer errors early in the development cycle.”

We are talking about developments that were implemented from approximately 2003 to 2015. A lot of time has passed since then. However, the concepts underlying these programming languages still look very progressive even today. We should thank the Microsoft Research team for collecting and publishing a large amount of material on the project’s website. I spent some time reading the articles and publications. While going through the information, I was interested in whether the languages from the “parallel realities” have influenced C# and .NET as we know them today.

After conducting some research, I found that there is indeed a positive influence. Although both Sing# and Spec# did not receive further development, successful ideas were subsequently implemented in the modern C# language. Today, we can confidently conclude that these concepts were implemented initially during work on experimental incarnations of the language:

Code Contracts;
Non-null reference types;
Readonly/pure methods.

Now I suggest taking a closer look at how each of the concepts mentioned above was initially presented and what implementation it has now.

Code Contracts

The Code Contracts project is a branch of Spec# and provides a way to define preconditions, postconditions, and object invariants in code [6]:

Preconditions are requirements that must be met when entering a method or property.
Postconditions describe expectations at the completion of the method or property code execution.
Object invariants describe the expected state of a class in its normal state.

The benefits of code contracts include the following:

Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.
Automatic testing tools: You can use code contracts to generate more meaningful unit tests by filtering out meaningless test arguments that do not satisfy preconditions.
Static verification: The static checker can decide whether there are any contract violations without running the program. It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.
Reference documentation: The documentation generator augments existing XML documentation files with contract information.

It should be noted that Code Contracts are no longer supported in .NET 5 and newer platform versions. Instead, it is recommended to use nullable reference types [6].

Looking at the Spec# specification, we will see the following definition [7]: “One of the basic units of specification in Spec# is the method. Each method can include a precondition, which describes the circumstances under which the method is allowed to be invoked, and a postcondition, which describes the circumstances under which the method is allowed to return. Consequently, an implementation of the method can assume the precondition to hold on entry, and a caller of the method can assume the postcondition to hold upon return. This agreement between callers and implementations is often known as a method contract”.

Thus, the concept of contracts is one of the fundamental principles for Spec# and has found its organic continuation in implementing code contracts.

Non-null reference types

In version 8 of the C# language, Microsoft introduced the concept of non-nullable references, which allows the developer to guarantee that a reference type cannot be null; it is achieved through compile-time checks, allowing for more straightforward and reliable programs.
The concept of non-null reference types also has its roots in Spec# and the idea of Code Contracts. For example, in Spec#, the declaration of a non-null reference looked like this:

It is worth noting that Tony Hoare, one of the creators of the ALGOL W programming language, claims that he was the one who proposed the concept of null references. And today, he believes that it was a “billion-dollar mistake” [8]: “I call it my billion-dollar mistake. It was the invention of the null reference in 1965. At that time, I was designing the first comprehensive type system for references in an object-oriented language (ALGOL W). My goal was to ensure that all use of references should be safe, with checking performed automatically by the compiler. But I couldn’t resist the temptation to put in a null reference, simply because it was so easy to implement. This has led to innumerable errors, vulnerabilities, and system crashes, which have probably caused a billion dollars of pain and damage in the last forty years.”

All developers who have ever encountered null pointer exceptions would agree with Tony on this.

“To make the use of non-null types even more palatable for migrating C# programmers, Spec# stipulates the inference of non-nullity for local variables. This inference is performed as a dataflow analysis by the Spec# compiler.” [9]

readonly / pure methods

In the ninth version of the C# language, the ability to declare readonly struct was implemented [10]. A structure declared with the readonly keyword guarantees that none of its elements would change the state of the structure. The readonly keyword can be applied to the entire structure and individual fields or methods.

Similar behavior was implemented in Sing# through the Pure attribute: a method is considered pure and declared as such with the Pure attribute if it returns a value without changing the state. Pure methods should not have side effects. [11]

Here I am drawing attention to another interesting point: functional programming is sometimes considered to be a synonym of pure functional programming, a subset of available programming that regards all functions as pure functions [12]. Recently, one can observe how functional programming concepts are actively entering and are being seamlessly integrated into the object-oriented languages we are accustomed to.

Conclusion

I fully admit that this list of examples of the influence of Spec# and Sing# on C# needs to be completed, and by studying the materials more carefully than I did, you can find other similar concepts at the genetic level of programming languages.

And to make it easier to study, I am attaching a list of valuable materials:

For real investigators — Spec# source code

Although the CodePlex site that hosted the Spec# project has closed, the source codes have been preserved on several mirrors:

Bibliography

Microsoft, “Singularity,” [Online]. Available: https://www.microsoft.com/en-us/research/project/singularity
H. С. Galen and R. L. James, “Singularity: Rethinking the Software Stack,” [Online]. Available: https://courses.cs.washington.edu/courses/cse551/15sp/papers/singularity-osr07.pdf
Wikipedia, “Spec#,” [Online]. Available: https://ru.wikipedia.org/wiki/Spec_Sharp
Microsoft, “Spec#,” [Online]. Available: https://www.microsoft.com/en-us/research/project/spec
Microsoft Research, “An Overview of the Singularity Project,” [Online]. Available: https://www.microsoft.com/en-us/research/wp-content/uploads/2005/10/tr-2005-135.pdf
“Code contracts (.NET Framework)” Available: https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts
K. R. M. L. and P. Müller, “Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs,” [Online]. Available: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml189.pdf
Null pointer, Available: https://en.wikipedia.org/wiki/Null_pointer#History
The Spec# Programming System: An Overvie. Available: https://www.cs.cornell.edu/courses/cs711/2005fa/papers/bls-cassis04.pdf
Microsoft, “Structure types (C# reference),” [Online]. Available: https://learn.microsoft.com/en-us/dotnet/csharp/language-reference/builtin-types/struct#readonly-struct
Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. Available: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml189.pdf
Wikipedia, “Functional programming,” [Online]. Available: https://en.wikipedia.org/wiki/Functional_programming
Code contracts (.NET Framework). Available: https://github.com/dotnet/docs/blob/main/docs/framework/debug-trace-profile/code-contracts.md
M. Lapierre, “Introducing Advanced Code Contracts with the Entity Framework and Pex. Available: https://www.codemag.com/Article/1001101/Introducing-Advanced-Code-Contracts-with-the-Entity-Framework-and-Pex