BosqueLanguage
The Bosque programming language is an experiment in regularized design for a machine assisted rapid and reliable software development lifecycle.
Install / Use
/learn @microsoft/BosqueLanguageREADME
Bosque Programming Language
This repository is archived and active development of the Bosque Language is moving to an external open-source repository under @BosqueLanguage (github repo is here)!
The Bosque Project
The Bosque Programming Language project is a ground up language & tooling co-design effort focused on is investigating the theoretical and the practical implications of:
- Explicitly designing a code intermediate representation language (bytecode) that enables deep automated code reasoning and the deployment of next-generation development tools, compilers, and runtime systems.
- Leveraging the power of the intermediate representation to provide a programming language that is both easily accessible to modern developers and that provides a rich set of useful language features for developing high reliability & high performance applications.
- Taking a cloud-development first perspective on programming to address emerging challenges as we move into a distributed cloud development model based around serverless and microservice architectures.
The Bosque Language is a novel hybrid of functional programming language semantics and an ergonomic block & assignment-based syntax. This allows developers to organize code into familiar/natural blocks and compositions while, simultaneously, benefiting from the correctness and simplicity of a functional programming model (see code examples below). The language also provides a range of ergonomic features for writing high reliability code, such as Typed Strings, unit typedecls for primitives, and first-class assertions/pre-post conditions/invariants.
The Bosque Testing Framework provides a built-in unit testing system, a powerful new SMT powered property-based testing system, and the ability to symbolically search for errors that can be triggered by user inputs in the entrypoints to the program (see the bosque command section below). These tests and checks can find compact debuggable inputs that trigger and error or failing test and, in many cases, can also prove that there will never be a case with a “small repro” that triggers the error!
The Bosque Runtime is a novel pathology free design that focuses on predictable latency, pauses, and 99th percentile behavior. This starts with a new garbage collector that is guaranteed to never need a stop-the-world collection, that only uses live-heap + a small constant in memory to run, and (will eventually) supports background external defragmentation! Beyond the GC behavior the runtime design excludes pathological regex behavior, dynamic execution bailout overload, and catastrophic amortized operation behaviors such as repeated rehashing (instead using slower but stable log time persistent structures).
The Bosque API Types provide a way to specify an application interface in a clean manner that is independent of the specifics of the Bosque type system. This enables the auto-generation of input validation and encoding logic. We currently support a universal JSON encoding but more efficient representations are possible. This design ensures that Bosque APIs can easily be integrated into polyglot systems (e.g. microservice architectures) or integrated into existing codebases (e.g. Node.js or C++).
The Bosque Package Manager (see the bosque command section) provides a centralized way to organize, test, and build an application – either as a standalone command or to integrate into other applications via JSON APIs. This manager is designed to take advantage of the checking capabilities of Bosque and will enable developers to (1) test against imported code using auto-generated mocks and (2) check that package updates do not (intentionally or maliciously) change the package behavior, introduce new data outputs, or expose sensitive data to unintended outputs!
Documentation
Small samples of code and unique Bosque tooling are below in the Code Snippets and Tooling sections. A rundown of notable and/or unique features in the Bosque language is provided on the Language Highlights page and complete documenation for the language and standard libraries are on the Language and Libraries doc pages respectively.
Detailed Documentation, Tutorials, and Technical Information:
- Language Highlights
- Language Docs
- Library Docs
- Runtime and GC Docs
- Tooling -- !TODO!
- Checkers -- !TODO!
- Tutorials - Coming Eventually!
- Technical Papers
- Contribution guidelines
Code Snippets
Add 2 numbers:
function add2(x: Nat, y: Nat): Nat {
return x + y;
}
add2(2, 3) //5
add2(x=2, y=3) //5
add2(y=2, 5) //7
All positive check using rest parameters and lambda:
function allPositive(...args: List<Int>): Bool {
return args.allOf(fn(x) => x >= 0i);
}
allPositive(1, 3, 4) //true
Tuples and Records:
function doit(tup: [Int, Bool], rec: {f: String, g: Int}): Int {
return tup.0 + rec.g;
}
doit([1, false], {f="ok", g=3}) //4
Sign (with default argument):
function sign(x?: Int=0i): Int {
var y: Int;
if(x == 0i) {
y = 0i;
}
else {
y = (x > 0i) ? 1i : -1i;
}
return y;
}
sign(5i) //1
sign(-5i) //-1
sign() //0
Nominal Types Data Invariants:
concept WithName {
invariant $name !== "";
field name: String;
}
concept Greeting {
abstract method sayHello(): String;
virtual method sayGoodbye(): String {
return "goodbye";
}
}
entity GenericGreeting provides Greeting {
const instance: GenericGreeting = GenericGreeting{};
override method sayHello(): String {
return "hello world";
}
}
entity NamedGreeting provides WithName, Greeting {
override method sayHello(): String {
return String::concat("hello ", this.name);
}
}
GenericGreeting{}.sayHello() //"hello world"
GenericGreeting::instance.sayHello() //"hello world"
NamedGreeting{}.sayHello() //type error no value provided for "name" field
NamedGreeting{name=""}.sayHello() //invariant error
NamedGreeting{"bob"}.sayHello() //"hello bob"
(Algebraic Data Types)++ and Union Types
datatype BoolOp provides APIType using {
line: Nat
} of
LConst { val: Bool }
| NotOp { arg: BoolOp }
| AndOp { larg: BoolOp, rarg: BoolOp }
| OrOp { larg: BoolOp, rarg: BoolOp }
& {
recursive method evaluate(): Bool {
match(this) {
LConst => return this.val;
| NotOp => return !this.arg.evaluate[recursive]();
| AndOp{_, larg, rarg} => return larg.evaluate[recursive]() && rarg.evaluate[recursive]();
| OrOp{_, larg, rarg} => return larg.evaluate[recursive]() || rarg.evaluate[recursive]();
}
}
}
AndOp{2, LConst{1, true}, LConst{1, false}}.evaluate[recursive]() //false
OrOp{2, LConst{1, true}, LConst{1, false}}.evaluate[recursive]() //true
function printType(x: Bool | Int | String | None ): String {
return match(x) {|
Bool => "b"
| Int => "i"
| String => "s"
| _ => "n"
|};
}
printType(1.0f) //type error
printType(true) //"b"
printType(none) //"n"
Validated and Typed Strings:
typedecl ZipcodeUS = /[0-9]{5}(-[0-9]{4})?/;
typedecl CSSpt = /[0-9]+pt/;
function is3pt(s1: StringOf<CSSpt>): Bool {
return s1.value() === "3pt";
}
ZipcodeUS::accepts("98052-0000") //true
ZipcodeUS::accepts("1234") //false
is3pt("12") //type error not a StringOf<CSSpt>
is3pt('98052'_ZipcodeUS) //type error not a StringOf<CSSpt>
is3pt('3pt'_CSSpt) //true
is3pt('4pt'_CSSpt) //false
entity StatusCode provides Parsable {
field code: Int;
field name: String;
function parse(name: String): Result<StatusCode, String> {
return switch(name) {|
"IO" => ok(StatusCode{1, name})
| "Network" => ok(StatusCode{2, name})
| _ => err("Unknown code")
|};
}
function accepts(name: String): Bool {
return name === "IO" || name === "Network";
}
}
function isIOCode(s: DataString<StatusCode>): Bool {
return s === 'IO'_StatusCode;
}
isIOCode("IO"); //type error not a DataString<StatusCode>
isIOCode('Input'_StatusCode) //type error not a valid StatusCode string
StatusCode::parse("Input") //runtime error not a valid StatusCode string
isIOCode('Network'_StatusCode) //false
isIOCode('IO'_StatusCode) //true
let ec: StatusCode = StatusCode{'IO'};
assert(ec.code == 1i); //true
Numeric Types
typedecl Fahrenheit = Int;
typedecl Celsius = Int;
typedecl Percentage = Nat & {
invariant $value <= 100n;
}
32_Fahrenheit + 0_Celsius //type error different numeric types
101_Percentage //invariant error
function isFreezing(temp: Celsius): Bool {
return temp <= 0_Celsius;
}
isFreezing(5) //type error not a celsius number
isFreezing(5_Celsius) /
