Microsoft Bosque Language

Automatic Verification
One of the advantages of a programming language that allows you to implement models based on formal reasoning is that this can be analyzed by tools that allow us to identify and eliminate errors through verification and validation processes. This improves the reliability of the execution's results. Some of the application settings could be as follows:

• Cryptographical protocols
• Implementation of finite state machines
• A network's mathematical models

Block Scoping
Local variables with block structured code is a very appealing model for structuring code. The Bosque language fuses functional programming with block scopes and {…} braces by allowing multiple assignments to updatable variables “var!”. This supports functional style programming in a block-scoped language and allows developers to write code such as:

function abs(x: Int): Int {
    var! sign = 1; //declare updatable variable with initial value
    if(x < 0) {
        sign = -1; //update the variable
    }

    return x * sign;
}

Reference Parameter Threading
Bosque language also allows developers to thread parameters via ref argument passing. This alternative to multi-return values simplifies scenarios where a variable (often some sort of environment) is passed to a method which may use and update it. Allowing the update in the parameter eliminates the extra return value management that would otherwise be needed:

function internString(ref env: Map<String, Int>, str: String): Int {
    if(env.has(str)) {              //use the ref parameter
        return env.get(str);
    }
    env = env.add(str, env.size()); //update the ref parameter
    return env.size();
}
...
var nameid = internString(ref env, "hello");

Typed Strings
Typed strings provide a novel mechanism for lifting known structure about the contents of a string into the type in a way that is meaningful to humans and that can be used by the type checker. This allows for code such as the following:

function foo(zip: String<Zipcode>, name: String) {...}

var zc: String<Zipcode> = Zipcode'98052';
var user: String = "Mark";

var zcbad: String<Zipcode> = "9"; //error not a typed string on right side
var zcbad: String<Zipcode> = "98052"; //error still not a typed string on right side
var zcbad: String<Zipcode> = Zipcode'9'; //error bad format in typed string literal

foo(user, zc) //Type error String not convertible to String<Zipcode>
foo(zc, user) //ok

Validating Program Behaviour
A central goal of the Bosque language is to simplify the process of building high reliability software. As part of this, the language provides first-class support for expressing a full range of invariants, sanity-checks, and diagnostic assertions.

entity Foo {
    field x: Int;
    invariant x > 0; //check whenever a Foo is constructed

    method m(y: Int): Int
        requires y >= 0; //precondition
        ensures _return_ > 0; //postcondition
    {
        check this.x - y > 0;   //sanity check - enabled on optimized builds
        assert this.x * y != 0; //diagnostic assert - only for test/debug
        return x * y;
    }
}

Recursion
As for recursion, things aren't too different in Bosque. The only new thing is the
recursive keyword, which informs us that a function is meant to be called recursively. This keyword is required both at the function definition and at the call. This may seem a little too problematic and frustrating, but there is a good reason to do this.

recursive function fibonacciNumber(n: Int): Int {
	return if (n == 0) 0
		elif (n < 3) 1
		else fibonacciNumber[recursive](n - 1) + fibonacciNumber[recursive](n - 2);
}

entrypoint function main(): Int {
	return fibonacciNumber[recursive](10);
}

None Processing
Handling none values is a relatively common task that can obscure the fundamental intent of a section of code with nests of cases and conditional handling for the special case. To simplify this type of code, Bosque includes various forms of coalescing or short-circuit operators to enable code like:

function foo(val?: {tag: Int, value?: String}): String {
    return val?.value ?| "[No Value]";
}

Bulk Algebraic Data Operations
Bulk algebraic operations in Bosque start with support for bulk reads and updates to data values. Consider the common case of having a struct with 3 fields where 2 of them need to be updated. In most languages this would need to be done on a field-by-field basis. However with the bulk data operations it is possible to perform the update as an atomic operation (unlike in an imperative style) and without manually extracting and copying fields (like in a functional style).

var x = {f=1, g=2, h=3};
x->update(f=-1, g=-2); //{f=-1, @g=-2, h=3}

Writing Comments
Bosque provides two types of comments that we can use interchangeably:

• Line comments, declared by the characters // at the beginning of a line
• Comment blocks, which will be framed between the characters /* at the beginning of the block and */ at the end

// This is an inline comment

/* This is
a multiline
comment */

Variable Declaration
Variable declarations in Bosque can be declared as constant in the scope using the “var” declaration form:

var x: Int = 3; //Int variable introduced and initialized
var y = 3;      //variable introduced and inferred to be of type Int

Alternatively variables can be declared as updatable in the scope using the “var!” declaration form. In the “var!” form an initializer expression can be used to set the initial value for the variable or it can be omitted to leave the variable uninitialized.

var! x: Int = 3; //mutable variable of type Int introduced
var! x = 3;      //mutable variable of inferred type Int introduced

Using Conditionals
Bosque provides if, elif, and else reserved words for writing a conditional block.
Additionally, due to Bosque being a curly-bracket language, we have to use curly brackets instead of a reserved word for closing blocks.

if ( x > 10 ) {
	return "error, greater than 10";
}
elif ( x < 0 ) {
	return "error, the number must not be negative";
}
else {
	return "it's ok, thanks";
}

Understanding Switch
Switch block allows us to execute different instructions according to the value of the variable. The wildcard _ will enable us to establish a flow for the values that do not correspond to any defined cases.

switch(x) {
    case 1 => { return "option one"; }
    case 2 => { return "option two"; }
    case _ => { return "any other option"; }
}

Writing Hello World

namespace NSMain;

entrypoint function main(): String {
    return "Hello World!";
}