Microsoft tiene documentación sobre lo que puede ser un nuevo lenguaje de programación. Su nombre es Spec#, pronunciado (spec sharp). El lenguaje fue diseñado para intentar ser una herramienta más efectiva en costos para desarrollar y mantener aplicaciones de alta calidad. Se puede escribir y buscar información, haciendo referencia a "specsharp" o "Spec# programming system". El entorno de programación cuenta con los siguientes componentes:

• El lenguaje de programación Spec# es una extensión del lenguaje orientado a objetos C#. Extiende el lenguaje al incluir tipos no-nulos y excepciones verificadas. Provee métodos que se contraen en forma de pre y post condiciones así como invariaciones de objetos.
• El compilador de Spec# se encuentra integrado dentro del entorno de desarrollo Microsoft Visual Studio para la plataforma .NET. El compilador implementa estáticamente tipos no-nulos, verifica los métodos en tiempo de ejecución (run-time), y almacena los métodos que se contraen como metadata para su utilización con herramientas downstream.
• El verificador estático de programas de Spec# (codename Boogie) genera condiciones lógicas de verificación desde un programa de Spec#. Internamente, usa un teorema automático que analiza las condiciones de verificación para comprobar la validez del programa o encontrar errores en eél.

Así como C# surgió como necesidad de contar con un lenguaje de altas prestaciones, Spec# es el complemento que hace más fuerte al lenguaje que es la competencia para Java.

Link: Spec# (MS Research)