A Vela program has no null pointers, no memory used after it is freed,
no value read before it is set, and no integer that wraps: the compiler
refuses what it can tell is wrong, and the program stops with a message
saying where for what only running it tells. This page lists those
rules, and the concerns neither settles yet, to come back to. Most of
the concerns are about places two names share. In Vela a value behaves
as a copy: giving it to a task, binding it to another name, or putting
it in a shape never lets two names change one thing. A few features give
that up on purpose, since they are how two names share one place: a
reference (flex&,
bind&, fixed&), a pointer
(^T), a shared field, a slice (a view of items in a region,
so a copy of it sees the same items), and a File (a copy
names the same open file). Nothing here changes the language.
Concerns: places two names share
A reference parameter changed through a pointer
open
The rule that a call gives a place it changes once compares the
places written at the call. A pointer reaches a place the call
doesn't write, so a task given &p^ as a
fixed& and p itself can change what
the reference reads:
shape Box
v: int
fi
task f(fixed& x: Box, flex p: ^Box@r)
p^.v = 99
show(x.v)
fi
task main()
region r
flex p = new Box(Box { v: 1 }) at r
f(&p^, p)
fi
Two pointers that hold one address slip past the same rule, since
the compiler can't tell they do:
task two(flex& a: int, flex& b: int)
a = 1
b = 2
show(a, " ", b)
fi
flex q = p
two(&p^.v, &q^.v)
The value an alters method is called on is given the
same way, so p^.set(p), where set writes
q^.n = 2 through the pointer it is given, reads
.n as 2.
- Why it is hard
-
Whether two pointers hold one address is known only when the
program runs. A rule written for the compiler has to be cautious:
it would refuse or warn about every call that gives a place behind
a pointer together with another pointer of that type, or into the
same region, most of which are fine.
- Ways it could go
-
A warning where a call gives
&p^ (or a part of
it) to a reference parameter and also gives a pointer of the same
type, or a place behind another pointer of it. Or, in a build for
finding mistakes, a check that the two addresses differ when the
call starts, trapping when they don't.
A reference to a shared field the task changes
open
A shared field that changes (shared flex) is one place
for the whole program, and every task can reach it by name. A task
given it as a fixed& reads it where it is, so its
own change to the field shows through the reference:
shape Tally
n: int
alters grow(flex m: [int: Tally]@r)
each i in 1..9
m[i] = Tally { n: 0 }
fi
.n = 9
fi
fi
task main()
region r
flex m = [0: Tally { n: 1 }] at r
m[0].grow(m)
show(m[0].n)
each k, v in m
m.del(k)
m[k + 100] = v
fi
fi
A plain parameter given a shared field is copied first, so it never
sees the change. A method called on a shared field is the same: in
Tally.last.bump(), a bump that sets
Tally.last to a new value reads the new one's fields
through .this.
- Why it is hard
-
The change may come from a task the body calls, or one that task
calls, so the compiler would have to know every shared field each
task can change.
- Ways it could go
-
The checker could learn, for each task, which shared fields it or
the tasks it calls may change, and refuse a call that gives one of
them to a reference parameter, as it refuses a place given twice.
A
shared read field, which only its shape's methods
change, narrows where to look.
A reference reads the place as it is now
by design
fixed& y = &x can't change x, but
it reads x as it is each time it is read, and
x may change between two reads:
flex x = 1
fixed& y = &x
show(y)
x = 2
show(y)
That is what a reference is for, and a
fixed& parameter is the same inside the task. What
the word promises is that the reader doesn't change the place, not
that nothing does. A reader who needs the value to stay as it was
keeps a copy: fixed v = y, or a
fixed x
parameter.
A place a lambda keeps, given beside it
open
A call never gives one place twice where one of them changes it (see
Places and regions). A
lambda that keeps a variable as a place,
[flex& count, @s], is a second name for it that the
call doesn't see, so it can be given beside the place itself:
task f(flex& x: int, g: [@s]() -> nothing)
g()
show(x)
fi
task main()
flex count = 1
region s
fixed g = [flex& count, @s]() -> nothing count = 5 fi
f(&count, g)
fi
No memory is misused: the variable outlives the lambda, and no
reference names an item of a slice that could move. But
x changes under f while
f holds it, as a reference's place may (above). A call could refuse a lambda that keeps a place it is also
given, where the compiler sees which places a lambda keeps; one
handed on through a variable or a parameter hides it.
Where a plain parameter is
warned
A plain parameter, x: T, is a copy, or for a value
larger than 64 bytes, the caller's own place. Its value is the same
either way, but what reads where the value is sees the difference:
&x, and == on a shape, an array, or a
tuple, which compare by where the value is. Such a read is a
warning that says which way the
compiler went; fixed x and
fixed& x say which is meant.
A method on an item of a slice that grows
open
An alters method called on an item of a slice changes
the item where it is. If the method makes the slice grow, through a
pointer to what holds it, the items move to a new block, and the
method's own change goes to the old one:
shape Bag
items: [Item]
fi
shape Item
n: int
alters poke(flex b: ^Bag@r, r: region)
b^.items.add(Item { n: 2 })
b^.items.add(Item { n: 3 })
.n = 9
fi
fi
task main()
region r
flex b = new Bag(Bag { items: new [Item]([Item { n: 1 }]) at r }) at r
b^.items[0].poke(b, r)
show(b^.items[0].n, " ", b^.items.len)
fi
No memory is misused, since the old block stays in the region until
it is freed, but the change is lost. The same item given to a task
as &b^.items[0] is refused, since a reference never
names an item of a slice; the value a method is called on isn't held
to that rule.
- Why it is hard
-
The slice grows through a pointer, which the rule that a place is
given once can't follow, and refusing every
alters call on an item of a slice would refuse the
common case, a method that touches only its own item.
- Ways it could go
-
Refuse an
alters call on an item of a slice when the
call also gives a pointer or region through which that slice could
be reached. Or have the method work on a copy of the item and
write it back to its index when the call ends. Or read the item
through the slice and its index at each use of .this.
A value in a map, while the map changes
open
A map's values are in its table, which moves when the map grows and
is packed again in place when most of its keys were taken out. So a
reference never names a value in a map (flex& v = &m[k]
is refused, as for a slice's item), and a slice never points into
one (m[k][0..2] is refused for an array value, whose
part would come to point at another key's value). Two uses aren't
held to that rule, and see the table as it was:
shape Tally
n: int
alters grow(flex m: [text: Tally]@r)
m["b"] = Tally { n: 0 }
.n = 9
fi
fi
task main()
region r
flex m = ["a": Tally { n: 1 }] at r
m["a"].grow(m)
each k, v in m
m.del(k)
m[k + "!" at r] = v
fi
fi
The first is the slice case above (a method on an item of a slice that grows): the method's change can be lost. The second is a loop through a
map that takes keys out and adds others: when the table is packed in
place during the loop, an entry can move under it, so it may see one
twice or skip one. No memory is misused either way, since a table
stays in its region until the region ends.
- Why it is hard
-
As for a slice, the map changes through a name the rule that a
place is given once can't follow. And a loop that sees each entry
once while the map changes needs the table to wait until it ends.
- Ways it could go
-
The ways listed for a slice's item. For the loop, packing a table
only by growing it into new room while a loop goes through it, or
refusing
m[k] = v and m.del(k) on the
map a loop goes through, as long as it can be told apart.
Copies of a map are one map
by design
A map value is a handle to its table, so every copy of it, a
variable, a field, an argument, names the same map, and a key one of
them adds is there for all:
flex a = ["x": 1] at r
flex b = a
b["y"] = 2
show(a.len, " ", a == b)
flex c = a.copy() at r
This is what Go does, and what copying a slice does for its items.
Copying every key and value at each assignment would hide a cost
that grows with the map; .copy() says when one is
wanted, and == says whether two names are the same map.
A copy of a slice shares its items
by design
A slice is a view of items in a region, a
twofold value, so a
copy of it, a fixed of it, or a parameter given it,
sees the same items, and a write through one is seen through all.
Nothing is written through a fixed name or a plain
parameter, at any depth, but a flex one that shares the
items may write them, and the fixed one sees the
change:
task change(flex xs: [int]@r)
xs[0] = 99
fi
task main()
region r
flex xs = new [int]([1, 2, 3]) at r
fixed seen = xs
change(xs)
show(seen[0])
fi
For the same reason, keeping a copy in a variable doesn't separate a
slice given twice to a call that changes it:
flex ys = xs and then
f(&xs, &ys) gives two views of the same items.
xs.copy() at r makes items of its own. A
flex copy that adds or takes out items stays linked or
not by where its items happen to be: an add that needs
more room copies the items to a block of its own, after which writes
are no longer seen, while one that finds room, and a
del, keep the two on the same items (see
Copies and parts), and the compiler
warns where a task leans on it (see
below). A bind slice never
adds or takes out items, so its copies stay on the same items, and a
task taking one as bind goes where a task type says
flex.
- Ways it could go
-
The given-twice message could suggest
.copy() at r when the place is a slice, and two
slices coming from the same variable could count as one place.
A [bind @r] lambda changes only what copies share
checked
A [bind @r] lambda changes only what every copy of it
shares: the items of a slice it keeps a copy of, a map, what a
pointer points to. Its own copy of anything else, a shape's field or
an array's item, it only reads, and the checker refuses a write
there, pointing to [flex @r]. So a copy of the lambda
changes nothing another copy wouldn't see anyway, and it is copied
freely: held in a field, given as a value, bound with
fixed. Calling one changes what it shares, so it is
called only through a flex or bind name,
as a slice's items change only through one, and it never keeps a
copy of what a fixed name owns (the author's decision, 2026-11-11;
until then it was held as a [flex @r] lambda is).
- What it costs
-
A lambda that changes a field of its own copy of a shape is a
[flex @r] one, held in one variable and never copied,
where it used to be a [bind @r] one.
A view after its slice changes
by design
warned
A part of a slice, xs[a..b], is a view of the items
where they were when it was taken. After del the items
move under it, and it may read one past the slice's new length;
after a growth that moves the items, it keeps viewing the old block:
region r
flex xs = new [int]([1, 2, 3, 4]) at r
fixed v = xs[2..4]
xs.del(0)
show(v[0], " ", v[1])
each v in xs is the same: it goes through the items
where they were when it started, as many as there were, so an item
deleted during the loop is still read.
each v in &xs goes through xs as it is
at each pass instead (see Arrays).
The compiler warns where a task does this: a copy or part used after
a del on the slice it was made of, an item written
through either after an add, and an add or
del on a flex slice parameter, once in
each task for each case (--repeat-warnings shows every
place; see Warnings).
- Ways it could go
-
The warning follows copies made in one task by a binding or an
assignment; it could follow slices in fields, given to calls, or
kept by lambdas, and a loop's next pass.
A copy of a File names the same open file
by design
A File is a value, and its open file belongs to the
region it was opened in, so a copy names the same open file. Closing
one closes it for both, and the other finds out only when a method
of its own runs:
include std/files {File, FileMode}
task main()
region r
flex a = File { path: "fa.txt" }
a.open(FileMode.Write) at r { failure e
show("no")
}
fixed b = a
a.close() { failure e
show("no")
}
b.write("x\n") { failure e
show("b: ", e)
}
show(b)
fi
Each open file has a number that changes when it closes, so no copy
ever reaches a file opened since (see
Regions and copies). Only the
state a copy shows is behind.
Threads later
Vela has no threads, so every change above happens at a point the
program's own order decides. Once two tasks can run at once, each
reference, pointer, and shared field is memory two threads may
change together, and the rule that a place is given once would have
to hold between threads as well as within one call. Whatever Vela
adds for running work at once (see
Events for one idea) will need its own
answer here before it is built.
Concerns: running
An error kept in a variable that is never read
open
A call written as a statement can't drop the error a
T ~ E may hold, and neither can binding it to
_. Binding it to a name that is never read does:
task main()
fixed x = int("oops")
show("went on")
fi
So does a flex given a new value before the old one was
read, and one of several results bound by name,
fixed a, b = int("7"), int("x").
- Why it is hard
-
Telling that a value is never read needs to follow every path
through the block: a
match, an is, or a
plan B on any of them reads it.
- Ways it could go
-
An error for a
T ~ E variable that no path reads
before it ends or is replaced. Or a warning for every variable
never read, which would catch this and more.
Running out of stack open
A task that calls itself without end, or an array too large for the
stack, stops the program with the system's own crash and no
vela: message:
task f(n: int) -> int
<- f(n + 1) + 1
fi
task main()
show(f(0))
fi
An array held by value lives on the C stack, so
flex big = [1#20000000] crashes the same way, as does a
new of a very large array, whose value is made on the
stack before it is copied.
- Why it is hard
-
How deep a program calls is known only when it runs, and the
stack's size is the system's. The checker allows an array of up to
1 TiB.
- Ways it could go
-
A limit on the size of an array held by value, pointing to a slice
for more.
new filling the array where it goes, rather
than copying one made on the stack. A handler for the crash that
prints vela: out of stack. A count of the call depth
in a build for finding mistakes.
A value made for one line lasts as long as its region
open
A region frees its memory all at once, when it ends. A value made in
it only to be shown or passed, and never kept, holds its memory
until then too:
task main()
region r
each i in 0..1000000
show([i, i + 1, ...] at r)
fi
fi
Nothing is read after it is freed, so this is memory held longer
than needed, never memory misused. A region made inside the loop
(region pass default) frees each pass's values as it
ends, which is how to write this today.
- Why it is hard
-
An arena frees everything it holds at once, not one value. And a
value given to a task that takes
[int]@r may be kept
by the task in something else in r, so only the
compiler's own uses (show, a comparison) are known to
keep nothing.
- Ways it could go
-
A value only shown or compared going in a hidden region freed when
its line ends, as the text
show builds for a value's
own str already does. Giving the space back when the
value is the last thing the region made, by moving the arena's end
back. A warning for a value made in a loop into a region the loop
doesn't declare.
Which of two stops comes first
by design
Calls, plan Bs, slice changes, and reading input run left to right,
but plain operators don't promise an order, so when two parts of one
expression would each stop the program, which one stops it isn't
defined:
flex xs = [1, 2]
flex i = 5
flex n = 9223372036854775807
show(xs[i] + (n + 1))
Either way the program stops, with a message saying where. Ordering
every part that may stop the program would take the C compiler's
freedom to arrange arithmetic (see
Current Limits).
nan compares with nothing
by design
A float that is nan (as
0.0 / 0.0 gives) is neither equal, similar, smaller,
nor larger than anything, itself included, as in C and every
language following IEEE 754:
fixed nan = 0.0 / 0.0
show(nan == nan, " ", nan ~= nan, " ", nan < 1.0, " ", nan >= 1.0)
So ~= isn't always true of a value and itself, and the
largest of a list holding nan depends on its order.
int(nan) stops the program.