Detailed contents — Lowent Manual

Skip to content

Lowent Manual←↑

Detailed contents

The contents opened out to the section level --- for going straight to a place.

Part I — Getting started

1 What Lowent sets out to do

1.1Can you tell from the head alone?1.2Five ideas 1.3One meaning, one spelling 1.4Where the language stands 1.5How to read this book

2 A first program — build, run, get rejected

2.1Building the tool 2.2hello, entropy 2.3Running it two ways 2.4How a contract stops execution 2.5Getting rejected 2.6--fmt fixes the shape 2.7Arguments and capabilities 2.8Common mistakes 2.9This chapter’s syntax at a glance

3 The surface — full stops, blocks and clause order

3.1The name first, then the arguments 3.2A free-standing full stop closes 3.3A block is always do … end 3.4Comments and literals 3.5Names 3.6Words are a budget 3.7The boundaries of the expr island 3.8Clause order in an op head 3.9Common mistakes 3.10This chapter’s syntax at a glance

Part II — Values and flow

4 Numbers — fixed-width integers and floating point

4.1Integer types name their width 4.2Widening is automatic, narrowing is written 4.3Overflow stops 4.4Division and remainder 4.5Booleans are not numbers 4.6Bitwise operations 4.7Floating point 4.8Common mistakes 4.9This chapter’s syntax at a glance

5 Ops — fn and proc

5.1Two kinds 5.2Purity is decided by observation 5.3Don’t write effects on a fn 5.4Effects spread to the caller 5.5Parameters and return 5.6Only neg is unary 5.7Modifiers 5.8Common mistakes 5.9This chapter’s syntax at a glance

6 Locals — let and var

6.1The word says whether it changes 6.2Write the type, or leave it to the value 6.3No name without a value 6.4How long a local lives 6.5if yields no value 6.6Common mistakes 6.7This chapter’s syntax at a glance

7 Flow — branches, loops and leaving early

7.1Conditions and loops 7.2guard — turning a condition into a fact 7.3Every path returns a value 7.4match — every case, none missing 7.5panic is an effect 7.6Common mistakes 7.7This chapter’s syntax at a glance

8 Expressions — prefix notation and the expr island

8.1Nothing to memorise in prefix notation 8.2The island’s precedence table 8.3What the island cannot do 8.4Short-circuiting guards conditions 8.5Expressions computed at translation time 8.6Common mistakes 8.7This chapter’s syntax at a glance

Part III — Data

9 Sequences — arrays and slices

9.1Start and length together 9.2Writing needs mut slice 9.3Narrowing the window 9.4Contracts remove bounds checks 9.5Common mistakes 9.6This chapter’s syntax at a glance

10 Aggregates — struct and enum

10.1struct — a collection of named fields 10.2enum — one of several 10.3Variants are closed with full stops 10.4Nothing may contain itself 10.5Common mistakes 10.6This chapter’s syntax at a glance

11 Types that hold answers — option and result

11.1option — a value, or none 11.2result and the errors clause 11.3try — passing failure upwards 11.4Crossing between the two channels 11.5Three ways to report failure 11.6Combining and nesting patterns 11.7Common mistakes 11.8This chapter’s syntax at a glance

12 Borrowing — ref and mut_ref

12.1Two kinds of borrow 12.2Write permission only narrows 12.3Many readers or one writer 12.4A borrow cannot outlive what it borrows 12.5There is no mut ref slice 12.6Common mistakes 12.7This chapter’s syntax at a glance

13 Named types — type, newtype, range, cast

13.1type is an alias, newtype a new type 13.2range — a contract that became the shape of a parameter 13.3cast — where a value may change 13.4bits — from 1 to 64 bits 13.5Pinning down byte layout 13.6Both directions of a layout, and a view that can fail 13.7bitset — a set of small numbers 13.8Scattered pieces as one view — segments 13.9Three kinds of type words 13.10Common mistakes 13.11This chapter’s syntax at a glance

Part IV — Contracts and effects

14 Contracts — write them, have them checked, lose the checks

14.1A contract is a checked promise 14.2Whose fault is it?14.3Contracts remove checks 14.4Conditions over every element 14.5Naming a contract 14.6Decide now what can be decided now 14.7Contract grades 14.8Build modes decide the remaining checks 14.9Common mistakes 14.10This chapter’s syntax at a glance

15 Effects — the marks an op leaves on the world

15.1Effects are closed words 15.2Effects spread to the caller 15.3Declared but not done is reported 15.4The effects line is a set 15.5via — a type argument decides the effects 15.6What purity allows 15.7Common mistakes 15.8This chapter’s syntax at a glance

16 Capabilities — power that is handed over

16.1Kinds of capability 16.2Capabilities travel down the chain 16.3Effects and capabilities are a pair 16.4Kind, not presence 16.5What the entry point receives 16.6Common mistakes 16.7This chapter’s syntax at a glance

17 Designing failure

17.1The boundary and the inside 17.2How to split an error enum 17.3Moving up the layers 17.4Where information may be thrown away 17.5Where panic is acceptable 17.6Common mistakes 17.7This chapter’s syntax at a glance

Part V — Memory

18 Regions — where values live, and memory reclaimed all at once

18.1Three places values live 18.2Opening a region and obtaining space 18.3Receiving a region 18.4Nothing is carried out of a region 18.5One cursor per root 18.6The growing root 18.7A stack on a region 18.8Common mistakes 18.9This chapter’s syntax at a glance

19 Ownership — one party responsible for disposal

19.1owned and drop 19.2Where branches meet 19.3Release and completion 19.4Not counting on the operating system to clean up 19.5At what strength is memory safety guaranteed?19.6Common mistakes 19.7This chapter’s syntax at a glance

20 Allocators and fixed memory

20.1The three parts of an allocator 20.2Cutting borrowed bytes 20.3Swapping allocators 20.4Default allocators that carve straight from a root 20.5Growing and returning a piece — grow and release 20.6Where the three layers sit in the standard library 20.7Who sets the size of the fixed window?20.8Same bits, different reading 20.9Common mistakes 20.10This chapter’s syntax at a glance

Part VI — Abstraction

21 Modules — hidden by default

21.1One file, one module 21.2Importing 21.3What can be exported, and how to shorten a name 21.4There is no search path 21.5When names collide 21.6Top-level order does not matter 21.7Common mistakes 21.8This chapter’s syntax at a glance

22 Generics — parameters fixed at translation time

22.1Taking values and types at translation time 22.2An instance per combination 22.3Putting conditions on types 22.4The type carries it, not a value 22.5Common mistakes 22.6This chapter’s syntax at a glance

23 Traits — one promise kept by many types

23.1What they are for 23.2Ops attached to types, and method 23.3Traits with several ops 23.4Signatures do not say fn or proc 23.5When a trait is not satisfied 23.6via self — more allocation effects only 23.7Common mistakes 23.8This chapter’s syntax at a glance

24 pipe — one line for each thing you mean to do

24.1The same work, two shapes 24.2Stages and terminals 24.3Walking once is the definition 24.4Reading only as much as needed 24.5The built-in map · filter with the same names 24.6Common mistakes 24.7This chapter’s syntax at a glance

Part VII — Concurrency

25 Actors — living with state, by messages

25.1Declare, make, talk 25.2Carrying values in messages 25.3Mailboxes — putting in and emptying 25.4Let it crash, then restart 25.5Where actors may be used 25.6Actors that hold a capability, and what state may contain 25.7Designing with actors — a transfer between two accounts 25.8Common mistakes 25.9This chapter’s syntax at a glance

26 Tasks and channels — exchange between bound flows

26.1Flows are bound to blocks 26.2Channels — containers with an order 26.3Deadlocks you can see from what is written 26.4Flows and memory 26.5What does not exist yet 26.6Common mistakes 26.7This chapter’s syntax at a glance

27 Parallel loops and atomic operations

27.1Declaring that a loop may be split 27.2The three conditions the processor checks 27.3The combining operation must be associative 27.4Atomic operations 27.5Memory orderings 27.6Lanes — computing several values at once 27.7Saying how a place is used — access 27.8Common mistakes 27.9This chapter’s syntax at a glance

Part VIII — The outside world

28 Input, output and files

28.1Standard output 28.2Reading a whole file 28.3What is opened is closed 28.4End and failure are different answers 28.5Triggering failure on purpose 28.6Common mistakes 28.7This chapter’s syntax at a glance

29.1Calling C — mark, right, effects line 29.2Types that cross the boundary 29.3C calls Lowent 29.4Callbacks and ownership 29.5Common mistakes 29.6This chapter’s syntax at a glance

30 Hardware — registers, interrupts, machine instructions

30.1The register map 30.2Access is enforced at translation 30.3Interrupt handlers 30.4What a machine supports — build tier 30.5Machine instructions — asm 30.6The absorbing boundary — where unsafe stops 30.7Using what the machine has — --hw 30.8Common mistakes 30.9This chapter’s syntax at a glance

31 Building and testing — packages, configuration, tests, cross-checks

31.1The manifest and the project 31.2Dependencies are pinned by hash 31.3A different program per build — build option and config 31.4Tests 31.5How the compiler is verified 31.6Asking where it is slow 31.7Common mistakes 31.8This chapter’s syntax at a glance

Part IX — The standard library

32 A map of the standard library

32.1Three layers — language, leaf, library 32.2What gets in 32.3The map by layer 32.4File names and module names 32.5Conventions every module follows 32.6The list of leaf ops — what lies beneath the modules 32.7Common mistakes 32.8This chapter’s syntax at a glance

33 Text and encodings — strings, fmt, utf8, codec, hash

33.1Cut, find, assemble 33.2UTF-8 — no replacement characters 33.3Hex and base64 33.4Hashes — three questions, three answers 33.5Regular expressions — no backtracking 33.6Common mistakes 33.7This chapter’s syntax at a glance

34 Containers and sorting — sortlib, sortgen, hashmap, vecgen, spsc

34.1Sorting and finding u64 34.2The type brings the criterion 34.3A hash map over the caller’s slice 34.4A growing generic vector 34.5A ring buffer passing values between flows 34.6Other containers 34.7Common mistakes 34.8This chapter’s syntax at a glance

35 Storage and handles — pool, shard, budget, wire

35.1Generational handles 35.2Brands — no mixing pools 35.3Non-overlapping pieces — shard 35.4Bit budgets — budget 35.5Bit fields — wire 35.6Other storage modules 35.7Common mistakes 35.8This chapter’s syntax at a glance

36 Input/output, networking, time, randomness, cryptography

36.1Buffered output — forget to flush and translation refuses 36.2Networking — handles are resources 36.3Randomness — reproducible sequences and operating-system entropy 36.4Time — monotonic clocks and wall clocks 36.5The HTTP request parser — its heart is rejection 36.6Cryptography — the order of the stack and the missing top 36.7Common mistakes 36.8This chapter’s syntax at a glance

37 The terminal — term and tty

37.1term does not write to the screen 37.2Redrawing only changed cells 37.3The number of cells is not the number of bytes 37.4Reading keys is computation 37.5Raw mode is a capability 37.6What is not built yet 37.7Common mistakes 37.8This chapter’s syntax at a glance

Part X — Grounds: what has been proven

38.1Tests show existence, proofs show absence 38.2Overlapping three layers 38.3What is proven 38.4Three ways of proving 38.5Promises this part keeps

39 The mathematical toolkit

39.1Six tools 39.2Sets and relations 39.3Partial orders — incomparable pairs 39.4Lattices and join — what to pick when combining 39.5Monotone functions and fixed points — why analysis stops 39.6Induction and invariants — dominoes 39.7Abstract interpretation — ranges instead of values 39.8Table of symbols 39.9How the tools interlock

40 Proofs about numbers — widening, narrowing, division

40.1Widening is a partial order 40.2Division and remainder 40.3Theorems that range provides 40.4Putting stopping into the model honestly 40.5What is not proven

41 Proofs about bounds — intervals, relations, row-major addresses

41.1Computing with intervals 41.2Relations — what intervals cannot do 41.3Four stages 41.4The row-major proof 41.5Trust proofs, but back trust with checks 41.6What is not proven

42 Proofs about ownership and borrowing

42.1Two machines and three events 42.2The central theorem 42.3Shapes rejected and shapes accepted 42.4Finding an implementation defect while widening the model 42.5Between model and implementation 42.6What is not proven

43 Loops and fixed points — proving “however many times”

43.1It breaks on the second round 43.2At a fixed point, any number of times 43.3Only one dangerous shape 43.4Fresh tokens — one move that removes the naming problem 43.5Nested loops — from function to relation 43.6What is not proven

44 Proofs about effects — writing “what it can do” into the type

44.1Effects are sets of atoms 44.2Four rules the processor enforces 44.3Capabilities — the partner of effects 44.4Effect soundness — not circular 44.5Optimisations relying on effects are legitimate 44.6What is not proven

45 Proofs about races and parallelism — discipline instead of a memory model

45.1The Bernstein condition — an answer from 1966 45.2Independence means no races, and the condition is necessary 45.3Between actors there is always a message 45.4Containment — where heavy tools are needed 45.5No races is not the same as deterministic 45.6What is not proven

46 Proofs about weak memory — with the default, you may think sequentially

46.1Sequential consistency and its counterexample 46.2An execution is a graph 46.3Impossible with the default, possible with relaxed 46.4Exactly that axiom forbids it 46.5Message passing — the weak ones exist for this shape 46.6Over all executions 46.7Weaker orderings add behaviours 46.8Seven tests from the literature 46.9What is not proven

47 Proofs about locks — where heavy tools are really needed

47.1The vocabulary of separation logic 47.2There cannot be two tokens 47.3Tools only as needed 47.4rwlock — two proofs of the same sentence 47.5Deadlock freedom and no starvation 47.6A borrowed proof in weak memory — spsc 47.7What is not proven

48 Proofs about syntax — whichever closer closes it, the same tree

48.1Algebra and denotation 48.2One statement is a one-statement block 48.3Closers do the same job 48.4Common mistakes 48.5What is not proven

49 Proofs about hashes — calling things by content, not name

49.1Hash functions and Merkle DAGs 49.2Called by content, not by name 49.3What changes a hash and what does not 49.4What can and cannot be proven 49.5What hashes stop 49.6What is not proven

50 What is not proven

50.1The trusted base — what proofs rely on 50.2The largest gap — between model and implementation 50.3What remains — by topic 50.4Not sold as “fully statically safe”50.5So what may you trust

Front and back matter

Appendix A — Words and builtins

The forty-three words Removed words Frequently used builtins Effects and capabilities

Appendix B — Diagnostics index

At translation time When execution stops Other diagnostics

Appendix C — Common mistakes and how to fix them

The surface Values and flow Effects, capabilities and memory Abstraction and concurrency

Appendix D — Grammar summary

Clause order of an op head Declarations Statements Patterns Expressions Heads and closers

Appendix E — Standard library modules

strings — string view operations

Design and boundaries Ops at a glance Ops in detail Using it Counter-examples Cautions

strbuf — owned string buffer and null-terminated cstr

Design and boundaries Ops at a glance Ops in detail Using it Counter-examples Cautions

fmt — formatting assembled into the caller’s buffer

Design and boundaries Ops at a glance Ops in detail Using it Counter-examples Cautions

utf8 — UTF-8 code point iteration and validation

Design and boundaries Ops at a glance Ops in detail Using it Counter-examples Cautions

utf16 — UTF-16 surrogate arithmetic

Design and boundaries Ops at a glance Ops in detail Using it Counter-examples Cautions

unicode — Unicode property tables

Design and boundaries Ops at a glance Ops in detail Using it Counter-examples Cautions

codec — hex and base64

Design and boundaries Ops at a glance Ops in detail Using it Counter-examples Cautions

regex — Pike VM regular expressions without backtracking

Design and boundaries Data structures Ops at a glance Ops in detail Using it Counter-examples Cautions

term — terminal renderer (the pure half)

sortlib — in-place quicksort

sortgen — generic sorting (the type brings the comparison)

searchlib — binary search on sorted slices

hashmap — u64 → u64 hash map

strmap — string-keyed hash map

vecs — growable byte vectors with caller-held buffers

spsc — lock-free SPSC ring buffer

hash — hashing (hash map slots · corruption detection · SHA-256)

math — floating-point maths

random — random numbers (reproducible sequences · OS entropy)

hmac — HMAC-SHA256 and HKDF

chacha — ChaCha20 stream cipher

poly — Poly1305 one-time authenticator

aead — ChaCha20-Poly1305 seal and open

x25519 — key agreement on a curve

aes — the AES-128 block cipher

gcm — AES-128-GCM authenticated encryption

crypto_hw — arithmetic the machine helps with

bigint — big-number modular arithmetic

rsa — RSASSA-PSS verification

p256 — the NIST P-256 curve and ECDSA verification

p384 — the NIST P-384 curve and ECDSA verification

ecdsa — ECDSA P-256 signing

ed25519 — Ed25519 signature verification

der — minimal DER parser

pem — unwrapping PEM envelopes

x509 — reading X.509 certificates

verify — certificate signatures and one link of a chain

A chain is a line of links ops Design

tls13 — the computational parts of TLS 1.3

tlssrv — the TLS 1.3 server handshake

tlscli — the TLS 1.3 client handshake

The order of the handshake ops Design

http — HTTP/1.1 request parser

soa — an SoA layout trial: one array per field

allocs — allocator traits, bumps and default allocators

pool — generational-handle block pool

shard — access units that split a store

budget — handle bit budgets and generation wraparound

wire — dividing one word into fields

flags — named on/off settings in one word

segarena — fixed-size segment arena

pagecache — page ids and pinning cursors

growvec — self-growing byte vector

vecgen — generic self-growing vector vec t a

mapgen — generic hash map table k v

nodelist — fixed intrusive lists

segview — cursors, total length and coalescing for segment views

lifemode · lifeatom — when a value ends

io — stream reading over slices

outbuf — buffered output where forgetting to flush is a compile error

files — file and directory streams where forgetting to close is a compile error

tty — terminal input

net — sockets (TCP loopback · in-process pairs)

clock — time and deadlines

trust — finding a trusted root in the trust store

It never holds the whole bundle ops

← PrevContents