> ## Documentation Index > Fetch the complete documentation index at: https://docs.canary.effectiveai.app/llms.txt > Use this file to discover all available pages before exploring further. # Language guarantees > What holds for every RSL program that passes the check, how the compiler establishes it, and what the language leaves out. 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: ```rsl theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} x: Num = self.a / (self.a - self.b), ``` > [accordion] divide/rater.rsl > > ```rsl divide/rater.rsl theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} > 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 > } > ``` ```sh theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} rslc check divide/rater.rsl ``` ```text theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} 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: ```rsl theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} x: Num = if self.a != self.b then self.a / (self.a - self.b) else 0, ``` > [accordion] guarded/rater.rsl > > ```rsl guarded/rater.rsl theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} > 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 > } > ``` ```sh theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} rslc check guarded/rater.rsl ``` ```text theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} 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`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#e-div-zero) | | A table lookup | A row exists for every key that can arrive | [`E-KEY-RANGE`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#e-key-range), [`E-LOOKUP-GAP`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#e-lookup-gap) | | `match` | An arm exists for every value | [`E-MATCH`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#e-match) | | A read of an `Option` | Both the present and the absent case have a value | [`E-OPTION-MATCH`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#e-option-match) | | `min`, `max`, `avg` over a list | The list holds one item or more | [`E-EMPTY-FOLD`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#e-empty-fold) | | `root`, `pow` | The operands are inside the function's domain | [`E-ROOT`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#e-root), [`E-POW-EXPONENT`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#e-pow-exponent) | | A date shift | The result is a calendar date | [`E-DATE-RANGE`](https://docs.canary.effectiveai.app/rsl/reference/check-messages/calculations#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: ```rsl theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} x: Num = self.y + 1, y: Num = self.x + self.a, ``` > [accordion] cycle/rater.rsl > > ```rsl cycle/rater.rsl theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} > 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 > } > ``` ```sh theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} rslc check cycle/rater.rsl ``` ```text theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} 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: ```rsl theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} x: Num = self.a / (self.b * self.b - 2), ``` > [accordion] conservative/rater.rsl > > ```rsl conservative/rater.rsl theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} > 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 > } > ``` ```sh theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} rslc check conservative/rater.rsl ``` ```text theme={"languages":{"custom":["languages/rsl.tmLanguage.json"]}} 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](https://docs.canary.effectiveai.app/rsl/explanation/checks-and-guarantees.md) 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](https://docs.canary.effectiveai.app/rsl/explanation/versions.md) explains each number. ## Related * [The type system](https://docs.canary.effectiveai.app/rsl/explanation/type-system.md) describes the types and the facts that the check tracks. * [Exact numbers](https://docs.canary.effectiveai.app/rsl/explanation/exact-numbers.md) explains precision and rounding. * [Check messages](https://docs.canary.effectiveai.app/rsl/reference/check-messages.md) explains each message, with a program that gets it and the fix. This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.