Language guarantees

RSL is a total, pure, statically typed language. It leaves out loops, recursion and side effects. In exchange, every program that passes rslc check has the properties on this page.

The guarantees at a glance

Question	Answer for a program that passes the check
Does it always return?	Yes. It holds a fixed set of calculations, and each one reads values that are computed before it.
Can it fail while it runs?	Each division, lookup, match and fold is shown safe for every input that the program accepts.
Is the result the same on every machine?	Yes. A result depends only on the request, and arithmetic is exact.
Can a value be missing?	Only as an `Option`, and each read of one handles both cases.
Can it change anything?	It computes its outcomes and has zero other effects: files, clocks and networks are out of reach.
How much work is one run?	The check prints a bound in terms of the sizes of the input lists.
Do numbers lose precision?	Numbers are exact rationals of any size. A value changes only at a `round` in the source.

A failure becomes a compile error

In most languages, a division by zero shows up when the program runs. In RSL, the check finds it in the source. This calculation divides by the difference of two inputs, each from 1 to 10:

x: Num = self.a / (self.a - self.b),

divide/rater.rsl

spec {
    rsl: "0.4.1",
    carrier: "Example Mutual",
    state: AZ,
    product: "Guarantees",
    effective_date: 2026-01-01
}

Sources = {
    manual: Source = {
        artifact: artifact("00000000-0000-4000-8000-000000000000"),
        kind: pdf
    }
}

Constants = {
    k [cite: manual:p1] = 3
}

Records = {
    Policy = {
        inputs {
            a: Num {precision: int} where self in [1, 10],
            b: Num {precision: int} where self in [1, 10]
        },
        step rating {
            x: Num = self.a / (self.a - self.b),
            premium: Premium [cite: manual:p1] = round(self.x * k, 2, half_up)
        }
    }
}

RatingOutcomes = {
    premium: Policy.premium
}

rslc check divide/rater.rsl

FAIL divide/rater.rsl (strict)
error: E-DIV-ZERO divide/rater.rsl:27:31: divisor `self.a - self.b` has range -9..9, which includes 0; guard the division (`if self.a - self.b != 0 then … else …`), or narrow the inputs it reads with a refinement
cost premium: 2 (each list of size 1: 2, 3: 2, 10: 2)

The check works out the range of the divisor from the ranges of its inputs, and that range holds 0. A guard removes the case. Inside the if, the check knows that the difference is nonzero:

x: Num = if self.a != self.b then self.a / (self.a - self.b) else 0,

guarded/rater.rsl

spec {
    rsl: "0.4.1",
    carrier: "Example Mutual",
    state: AZ,
    product: "Guarantees",
    effective_date: 2026-01-01
}

Sources = {
    manual: Source = {
        artifact: artifact("00000000-0000-4000-8000-000000000000"),
        kind: pdf
    }
}

Constants = {
    k [cite: manual:p1] = 3
}

Records = {
    Policy = {
        inputs {
            a: Num {precision: int} where self in [1, 10],
            b: Num {precision: int} where self in [1, 10]
        },
        step rating {
            x: Num = if self.a != self.b then self.a / (self.a - self.b) else 0,
            premium: Premium [cite: manual:p1] = round(self.x * k, 2, half_up)
        }
    }
}

RatingOutcomes = {
    premium: Policy.premium
}

rslc check guarded/rater.rsl

PASS guarded/rater.rsl (strict)
cost premium: 2 (each list of size 1: 2, 3: 2, 10: 2)

The same rule covers each operation that can fail:

Operation	What the check establishes	Message
`a / b`	`b` is nonzero	`E-DIV-ZERO`
A table lookup	A row exists for every key that can arrive	`E-KEY-RANGE`, `E-LOOKUP-GAP`
`match`	An arm exists for every value	`E-MATCH`
A read of an `Option`	Both the present and the absent case have a value	`E-OPTION-MATCH`
`min`, `max`, `avg` over a list	The list holds one item or more	`E-EMPTY-FOLD`
`root`, `pow`	The operands are inside the function’s domain	`E-ROOT`, `E-POW-EXPONENT`
A date shift	The result is a calendar date	`E-DATE-RANGE`

Every program finishes

RSL has zero loops and zero recursion. A calculation reads other calculations, and a chain of reads that returns to its start is an error:

x: Num = self.y + 1,
y: Num = self.x + self.a,

cycle/rater.rsl

spec {
    rsl: "0.4.1",
    carrier: "Example Mutual",
    state: AZ,
    product: "Guarantees",
    effective_date: 2026-01-01
}

Sources = {
    manual: Source = {
        artifact: artifact("00000000-0000-4000-8000-000000000000"),
        kind: pdf
    }
}

Constants = {
    k [cite: manual:p1] = 3
}

Records = {
    Policy = {
        inputs {
            a: Num {precision: int} where self in [1, 10],
            b: Num {precision: int} where self in [1, 10]
        },
        step rating {
            x: Num = self.y + 1,
            y: Num = self.x + self.a,
            premium: Premium [cite: manual:p1] = round(self.x * k, 2, half_up)
        }
    }
}

RatingOutcomes = {
    premium: Policy.premium
}

rslc check cycle/rater.rsl

FAIL cycle/rater.rsl (strict)
error: E-CYCLE cycle/rater.rsl:27:13: attribute dependency cycle: Policy.x -> Policy.y -> Policy.x; every rating would fail at runtime. Compute the shared value in its own attribute so that no attribute needs itself

A list function such as sum visits each item of an input list once. So the work of one run has a bound in the sizes of those lists, and a passing check prints it on its cost line.

The checker is conservative

The check accepts a program only when it can show each operation safe. It refuses some programs that are safe:

x: Num = self.a / (self.b * self.b - 2),

conservative/rater.rsl

spec {
    rsl: "0.4.1",
    carrier: "Example Mutual",
    state: AZ,
    product: "Guarantees",
    effective_date: 2026-01-01
}

Sources = {
    manual: Source = {
        artifact: artifact("00000000-0000-4000-8000-000000000000"),
        kind: pdf
    }
}

Constants = {
    k [cite: manual:p1] = 3
}

Records = {
    Policy = {
        inputs {
            a: Num {precision: int} where self in [1, 10],
            b: Num {precision: int} where self in [1, 10]
        },
        step rating {
            x: Num = self.a / (self.b * self.b - 2),
            premium: Premium [cite: manual:p1] = round(self.x * k, 2, half_up)
        }
    }
}

RatingOutcomes = {
    premium: Policy.premium
}

rslc check conservative/rater.rsl

FAIL conservative/rater.rsl (strict)
error: E-DIV-ZERO conservative/rater.rsl:27:31: divisor `(self.b * self.b) - 2` has range -1..98, which includes 0; guard the division (`if (self.b * self.b) - 2 != 0 then … else …`), or narrow the inputs it reads with a refinement
cost premium: 2 (each list of size 1: 2, 3: 2, 10: 2)

For a whole number b, the divisor is always nonzero. The check tracks one range for each value, and the range from -1 to 98 holds 0. A guard on the divisor, or a narrower input, gives the check the fact it needs. The check keeps these facts about a value: its range, its decimal precision, a finite set of values, nonzero, non-empty, and present. It runs in one pass, so the same source always gets the same messages.

How each guarantee is established

Guarantee	Established by
A program returns, has zero outside effects, and gives the same result everywhere	The language itself: it has zero constructs for loops, recursion, input, output, clocks or mutation
A program is free of failures while it runs, and each value has its declared type	The checker. Each of its rules has a test that accepts a program and a test that refuses one. The checker itself is unproven.
Rounding behaves as written	Machine-checked proofs, in Lean, of properties of each rounding mode, of root bounds and of stepwise sums

A failure that the checker misses stops that one rating with an error, in place of a premium.

What RSL leaves out

General computation. RSL has zero loops, recursion or user-defined functions. A program is records, tables, rules and calculations.
Text. A value is a number, a date, a Bool, an enumeration member or a code with a pattern. Free text is outside the language.
Input and output. A program reads its request and its own tables.
Unit checking. Premium, Rate, Factor and Pct name the role of a number. A premium plus a factor compiles.
Proof that a program matches its source documents. The check requires a citation for each filed number, and a reviewer reads the cited page. Checks and guarantees lists what a review still covers.
A stable 1.0. A file names its language version, and this compiler reads versions 0.4 and 0.4.1. Versions explains each number.

The type system describes the types and the facts that the check tracks.
Exact numbers explains precision and rounding.
Check messages explains each message, with a program that gets it and the fix.

Get started

Tutorials

Implement a filing

Test a rater

Quote and underwrite

Concepts

Reference

Language guarantees

The guarantees at a glance

A failure becomes a compile error

Every program finishes

The checker is conservative

How each guarantee is established

What RSL leaves out

​The guarantees at a glance

​A failure becomes a compile error

​Every program finishes

​The checker is conservative

​How each guarantee is established

​What RSL leaves out

​Related

The guarantees at a glance

A failure becomes a compile error

Every program finishes

The checker is conservative

How each guarantee is established

What RSL leaves out

Related