Austral: A systems language with linear types and capabilities
borretti.me
borretti.me
I am really intrigued by your explicit anti-features list. They are very close to my preferences for language design, so I was going to keep on reading just from that. The feature list is spelled out well and I certainly think you managed to make this article a nice hook for looking further.
Then I followed a link to the language spec. My god, but is it not only written cleanly, but the presentation is so clean too. I got a short way in (after jumping to the type system specification) and stopped to come comment. I doubt you were expecting to get compliments for layout and formatting, but I am going to shamelessly steal your spec’s presentation for my language docs.
>So, I’m just going to read the compiler source and then get a hold of you later.
Luckily, the entire linear type checker is just 600 lines of code: https://github.com/austral/austral/blob/master/lib/Linearity...
600 lines of code in an extremely high level and very powerful language.
Curious to see it implemented in Austral.
As many things go, the Smalltalk designers had this insight a few decades ago, all "binary messages" have the same precedence.
I still think it's weird, but it makes sense.
The other way around.
A "binary message" is specifically the message of binary operators. Smalltalk also has unary messages (named messages with no parameters), and keyword messages (non-binary messages with parameters).
Its precedence rules are unary > binary > keyword, and left to right.
So
foo bar - baz / qux quux: corge
(((foo bar) - baz) / qux) qux: quux
a b; c
a b.
a c
foo + bar qux; quux
foo + bar qux.
foo quux
foo + (bar qux); quuxSmalltalk-76 introduced a fixed syntax and does have a bit of precedence: unary > binary > keywords. All binary messages have the same priority, which given that you can define new ones avoids a lot of complexity at the cost of a few extra parenthesis.
Shame the examples are a bit too simplistic to show the value of linearity e.g.
function closeFile(file: File): Unit;
It would also demonstrate runtime error handling, which is completely ignored by the entire document and largely absent from the spec (error handling is discussed a lot, but never actually demonstrated).
The only document I found was https://austral-lang.org/tutorial/errors which seems to indicate that not only does Austral (unfortunately imo) follows Haskell's lead through using an Either for errors (which is clear as mud), it proceeds to break Haskell's mnemonic for success/failure (not that that's great, but at least it was something).
Realistically, it shouldn't, and there's no way you would be able to handle it properly even if it did. Flush your FDs to ensure you get write errors before closing. And EBADF means there's a bigger problem in your program (you're incorrectly sharing FDs).
File openFile(String path)
File writeString(File file, String content)
Opening or writing a file can reasonably fail in multiple ways.
The language does not handle any failing effects at all.
But than this should be communicated adequately, imho.
(And better, more realistic examples, that aren't glaring wrong, would be a good idea. But I fear all examples would than melt down to pure functions. But pure functions were never an issue. In any language).
I really understand why someone would try to build a better language. All the premises in the blog post are right! Only that I fear that the conclusion are frankly quite off. Looks like the usual misunderstanding of "KISS" to me, to be honest.
(And I don't like to be to harsh actually. I know how much work it is to come up with anything that works at all. Languages are a very unrewarding field of work sadly).
>(Error handling etc. omitted for clarity.)
I've thought about this at length. The conclusions are right.
You wrote that in a later example, after several simpler examples not including error handling either, and not introducing error handling at all. In fact error handling is not covered anywhere by the introductory text.
The part which really grates is that this makes all the examples in the "motivation" section for linear types work against their very section: because all the destructors are infaillible, they're perfect motivations for an affine type system and implicit destructors, all they say is that a linear type system requires more work from the user for no visible value.
With affine types, destructors must be infallible, otherwise you get the double throw problem, as in C++ or Rust.
With error handling, the signatures would just be:
function closeFile(file: File): Either[File, Unit];
That's literally my point, and what you are not demonstrating in this introductory text, and what the examples you wrote completely undermine.
> With error handling, the signatures would just be:
But they're not is the point, the text spends an entire section and a good 10 pages explaining linear types (thus clearly assuming the reader does not know about them), yet all the examples undermine what they're supposed to defend. If being already sold on linear types is necessary to be motivated by this section it's not doing a very good job.
And, again, no coverage or explanation of error handling anywhere in the introductory text, even though that's as important as it's divisive (even more so for a language focused on safety and correctness).
As originally noted I had to go hit up section 14 of the tutorial (and I can't say I'm impressed by the coverage that document provides, as it spends more time expounding about the philosophical categorisation of errors than actually demonstrating error handling capabilities and features).
> Where returning a `File` means closing it failed.
That's not a very useful error report, and probably wrong as well: in most situations the file handle is invalidated by closing it, even if the closure fails.
In POSIX, "EBADF" reports that the file was already broken, and "EIO" reports a flush error, which usually means that the resource has gone away e.g. it was on a transient or network device which is inaccessible.
"EINTR" is the only one for which is debated[0] and may leave the fd open, but even then whether any operation other than closing (again) can succeed in that case is not clear.
Together with this joke to call async a "fashion" (in a time of networked services everywhere, and high performance I/O being now only possible with asynchronous APIs) this whole thing will go nowhere, imho.
Nice theoretical ideas aren't enough when it comes to programming languages. The execution is key.
This thing is a clear instance of misunderstanding of "the KISS principle": Dumbing things down to the max is not KISS! Because it neglects inherent complexity. KISS only wants to remove accidental complexity. All other complexities still need to get addressed accordingly. Nobody needs the next Go or V.
The OP is complaining about the introductory code samples and how they don't demonstrate the error handling idioms of the language, not any problems with how errors are handled in this language.
Write might be similar. I think you want to return a file on success and some information that you might be able to do something with on failure, where there might be a path to retrieving a working file from it.
Easier to see, allocate could return a MaybeHeap which you branch/match on, where one path is call a garbage collector and try again.
This is all kind of messy though. Retry loops or memory cleanup attempts should perhaps be on the far side of the API.
Rust throws an exception if things go too badly wrong as far as I can tell, though the docs tell me panic! isn't an exception, and also how to catch it.
So you think it is better to continue execution completely oblivious of the issue? Or do you assume `close` will straight up terminate the program if it fails?
> Flush your FDs to ensure you get write errors before closing.
Nothing precludes implementing `closeFile` by flushing it, returning any error as a failure, then actually closing.
I love many of the choices here, like removing implicit type coercion, type inference, and operator precedence. I do worry that it could go too far. One thing we see with Go is that the simplicity of the language, while it has many virtues, also leads to some crude designs that feel regressive. For example, treating errors as values is a fine idea, but the language is too rudimentary to express sum types, so the handling of errors becomes crude and cluttered. Not bad enough to ruin the language, but bad enough to be an annoying wart. I hope that Austral can avoid falling into such traps when it needs to tackle more advanced concepts such as concurrency (I don't know how this is done today?). Not having async/await is fine, for example, provided that there is some other mechanism that doesn't lead to spaghetti code or too much repetition.
The part I'm the least enthusiastic about is the Algol/Ada-style syntax. I'm not sure the added verbosity of that syntax is superior to C-style syntax. The language I use the most these days, Go, is essentially Modula/Oberon with C-style syntax and no semi colons, both of which I think improve the ergonomics.
For example, Rust-style iterators are "complex", yet they cause less errors than explicit indexing. Their combinators, that afford a lot of their expressivity, would cause very difficult to write types without type inference.
There's a similar tale of expressivity vs simplicity in the current implementation of the borrow checker in rust that is not using lexical (tied to a syntactic scope) lifetimes. For having used rust before non lexical lifetimes were a thing I can guarantee that from a user's point of view it is worth all the complexity in the rules and the implementation. I also have a hard time to imagine a serialization framework like serde without the ability to derive traits with an annotation.
Separating interface and implementation opens up to (compile time, fortunately) errors when they don't match, and brings no gain: the public interface can be generated by tools like cargo doc.
Ada style syntax I find difficult to read (I prefer braces) but this is purely a product of familiarity I think
The document also says the language does not feature unwinding panics. What does it has then?
The capability system is interesting, but I am surprised in the hello world example that printing to the console doesn't seem to require a dedicated capability.
I think an extension to this capability system would be some sort of tie-in with the OS so that a given process can start with only a subset of the root capability
It's half the reason to dislike C/C++'s module... err, text inclusion system. The other half being horrible build systems/times.
The only way it'd be halfway reasonable is if there was very good editor support for syncing the two copies. And even then, what's the point of denormalizing your source code? Like you said, you can always generate docs from source or an interface file from source (if for some reason you were building a closed source module -- which seems very much not the norm these days).
For example, real filesystems are complicated and quirky.
Though it's risky to build on another experimental language, it seems like building on Zig's toolchain would be a good way to get lots of cross-platform capability and experience quickly, since it accepts C and generates code for many platforms.
In a capability based system, you should present a set of directory capabilities to a process on launch, and the process should be able to access files/subdirs, or create new files/subdirs within it, and potentially pass capabilities to those files to other processes. The app should not, however, be able to escape the directories it has capabilities to. There should be no way to go "up". The only way a process should gain access to another directory is if another process explicitly passes it the capability. This should really be enforced at the OS level, but it is not (usually). If a capability based language can enforce it in its runtime/stl, then you can at least not have to worry about programs written in those languages escaping their directories (assuming no unsafe/FFI).
As someone who is also bootstrapping things, I just want to point out this is not the encouraging comment you might think it is. 'How can I help?' is.
The maintainer of a project puts in the work of designing it, developing it, documenting it, and publicizing it... the last thing they want to hear is "cool, just keep doing that forever until it's good enough for me to adopt wholesale without lifting a finger".
If it motivates you, you're in for disappointment.
1. "How can I help" but it's a lie.
2. Silence.
Nowadays, I need to pull larger-scale integrations of libraries together, and the quality of the supply chain along with productive development practice occupy my mind. I suppose I wouldn't be out of my depth to work on the Jetbrains IDE plugin.
I tend to buy licenses for tools I use (Sublime), I'd help a Patreon. If this could acquire foundation support like Rust did, it might reach a similar position.
But I agree that “linear types” is not a great name. Something like “single use types” would be clearer to me.
This talk explains some other origins as well as the connections between different logics to different type systems (though the focus is on stack languages) https://youtu.be/_IgqJr8jG8M
There's also "affine logic" which riffs on the same thing.
It's not great because it can scare away programmers who hear "linear" and think abstract nonsense. But there's not really a better name. "Uniqueness type" or "Single-use type" is too verbose. I'd rather not bikeshed the terminology too much and just use what exists.
”Single-reference”?
That's exactly the property linear typing enforces: a new binding only appears once on the right hand side, ie. let x = v in e, where e references x only once.
> "La logique linéaire est issue d'une prise en compte systématique de l'interprétation catégorique. En particulier, les espaces cohérents [...], proches des espaces vectoriels [...] font apparaître des structures logiques familières en algèbre linéaires [...]"
> Translation: "Linear logic developed from systematically taking into consideration the categorical interpretation. In particular, coherent spaces [...], similar to vector spaces [...] give rise to logical structures which are familiar from linear algebra."
> So, in one sentence, it is called linear logic because it involves semantics which resemble structures from linear algebra.
https://math.stackexchange.com/questions/2339147/why-is-it-c...
Does every linear value ultimately have to be passed to an extern function that doesn’t follow the linear typing rules?
Whatever underlying value would be moved out of the linear record by destructuring (and thus consuming) it, then released via the underlying platform's operation (e.g. close(2), CloseHandle, ...)
edit: from the linked section, it looks like field access is a linear operation:
> when you have a linear record type, you can’t extract the value of a linear field from it, because it consumes the record as a whole, and leaves unconsumed any other linear fields in the record
so for a "newtype" (a single field wrapper type) you can just access the one field, maybe.
As long as there is interface/implementation separation, no interface that gives you the underlying handle and not enough reflection in the language to dig it out, you're solid.
Open and close must both be on the inside of the implementation so can breach the abstraction.
Two nitpicks from my side.
From the anti-goals:
> Async is a very specific feature, and every way of doing concurrency other than kernel threads has come and gone out of fashion (think Scala actors and Goroutines, two very admirable features)
Scala actors are not a language feature so are not remotely comparable to async/await or Goroutines. They are also not "out of fashion", if anything they were just overused - but it doesn't impact the language in any way at all.
> no context-sensitive syntax
There are different opinions on language design and that's fine. But "ease of use" and "complex systems" are not at adds. In fact, you can argue that Assembly is a "simpler" system than Austral. But does that make it easier to use? I don't think so. I think this part sheds light on the fact that the author needs to work on that part - not necessarily on changing the language design, but at least the language isn't great.
> having everything be explicit causes complexity to be foisted on the user
> I'd rather my systems language scale between contexts.
I might need more control in a kernel. Userspace support code benefits from being in the same language and needs some systems programming features but doesn't need as much control.
I also find writing tools in Rust to be a joy.
Depending on the user, this is a plus. For a system language is important to be pedantic and explicit at each corner. HOW MUCH is the question! but the point of experiments like this is see how much you can go and still keep the pain low!
P.D: "Complexity" can be good, but "Complicated" is what is to be avoided. I prefer to eat the complexity of Rust rules than the complications of debug a thread code...
Options I'm aware of are die (optionally gracefully), allocate more stack (segments or moving), allocate a lot of address space up front and then die on exhaustion.
Asking because I think there's a reasonable argument that out of heap and out of stack are the same category, and the docs discuss returning optional from allocating functions, but not tagging all functions with an optional to indicate out of stack.
As someone famous in CS once said, “simplicity is a great virtue but it takes hard work to achieve it and education to appreciate it.”
Let’s face it: programming is hard and no amount of waving our hands and refusing to learn anything new is going to make anything better.
If this linear type system is great, skip to why it’s great.
Again, a lot of neat ideas in here. The parser is a good idea. Langsec and a security focused language is nice to see!
This somewhat exists as `must_use`: https://doc.rust-lang.org/std/hint/fn.must_use.html
>One key obstacle to this is that Rust supports panics anywhere-- there's no provision for "panic-free" code as of yet-- and a panic might need to drop values as part of unwinding the stack.
Yes, there's a fundamental incompatibility between linear types and traditional exception handling. This was a big question I had to think about and answer in the design.
Basically: Rust has "affine" types (a weakening of linear types) where values can be silently discarded. The compiler inserts destructor calls (whose behaviour is customized in the `Drop` trait). The compiler also emits the exception-handling code so that when a panic is thrown the stack unwound and the destructors are called.
This approach is incompatible with linear types (linear types don't privilege any one function as the destructor). So linear types are incompatible with traditional exception handling.
The choice, then, is: keep linear types or keep traditional exception handling. I decided to keep linear types, because they're simpler.
The full rationale is elaborated at length here:
Nice to see this spelled out. If the instance can be summarily dropped without error you can throw past it, and ideally call it affine instead of linear.
If the instance needs that close() call, you either can't throw past it, or you need to move the live instances into the exception instance as it passes by and deal with them at the catch site. I found a paper discussing that somewhere but didn't keep a reference to it.
A possibly interesting compromise is to allow linear types, but their live range cannot contain an unknown function call, or a function call coloured with throws. That models holding on to some handle and not doing anything too hazardous until you can put it away safely.
- your blog "hides" the links behind barely visible font changes, quite funny for someone who designed a programming language with no hidden function call.. Don't do this please.
- the "Arithmetic Expression" section talk about integer division overflows but not about the other overflows?
- I couldn't understand the "Cast Expression" section, either it's me or it has to be clarified.. Also a syntax remark: I'm surprised that there is no easily greppable keyword for casting.
- two other comments about syntax:
1) the '!' symbol is used to dereference and in "read-write borrow", I don't see any obvious relationship between both usage, maybe you could use '@' for dereference ?
2) how about using <> for not equal insteal of /= ? The "C programmer I am" read "a /= b;" as "a = a / b;" ..
What if you somehow mark the close() function as--let me make up a name--a "destructor". Then enforce at compile time that a value must always have a call to a destructor (or maybe it gets called automatically when out of scope).
1. Does that solve the close problem as well as linear types?
2. Do linear types solve other problems that the above doesn't?
No, because if pointers are copyable, multiple places can point to the same memory address, and all destructor guarantees are gone. You then have use-after-free vulnerabilities, that is, a CVE.
C++ has had RAII for 30 years. It is demonstrably, empirically not good enough.
>2. Do linear types solve other problems that the above doesn't?
Linear types give you:
1. Capability-based security.
2. The ability to enforce high-level, state machine-like protocols (see the database access example) at the type level.
3. Code that performs fast in-place mutation while maintaining a purely functional interface.
This seems orthogonal to me. If you allow pointers, then linear types don't help you either, right?
But if the compiler can verify that a value is used exactly once, then why can't it verify that a value is destructed? We mark a function as a destructor and the compiler verifies that the value is passed to a destructor exactly once.
> 1. Capability-based security.
I'm probably missing this, but this also seems orthogonal. It seems like Capabilities are implemented with different types. The Filesystem type is different from the Path type, and you get different capabilities depending on which type you get. This has nothing to do with linear types.
> 2. The ability to enforce high-level, state machine-like protocols (see the database access example) at the type level.
I'd like to know more about this, because it sounds cool.
> 3. Code that performs fast in-place mutation while maintaining a purely functional interface.
This also sounds cool. Do you have a code example off the top of your head?
Unsafe pointers should exist at the FFI boundary and be wrapped in a linear API. Every language has a "escape hatch" for this purpose, and you ultimately have to rely on practices to constrain it. You can call malloc in any language.
>But if the compiler can verify that a value is used exactly once, then why can't it verify that a value is destructed? We mark a function as a destructor and the compiler verifies that the value is passed to a destructor exactly once.
The problem is the compiler can't verify it. In a Turing complete language, it's simply impossible to do it in a general way without restrictions. Every language that has compile time memory safety (Austral, Rust, Cyclone, a few others) imposes restrictions to make the analysis tractable.
>I'm probably missing this, but this also seems orthogonal. It seems like Capabilities are implemented with different types. The Filesystem type is different from the Path type, and you get different capabilities depending on which type you get. This has nothing to do with linear types.
Capabilities have to be linear so that they can't be copied surreptitiously:
https://austral-lang.org/spec/spec.html#rationale-cap
>I'd like to know more about this, because it sounds cool.
There's some examples in the post. The state machine is the state of the file handle and the linear types ensure only valid transitions can be used.
>This also sounds cool. Do you have a code example off the top of your head?
Not something existing I can point to. But if you have a function:
generic [T: Type]
function reverse(list: List[T]): List[T]
Even when you could verify this, it wouldn't prevent use after free bugs.
That is, an implicitly invoked destructor is not an UAF concern.
No.
> 2. Do linear types solve other problems that the above doesn't?
Yes: destructors which can fail. This is an issue in C++ and Rust. For instance, in most OS closing a file may return an error. With an implicit closure, that is not an information you can retrieve, you have to know that an error can occur, figure out that you might be interested, and add non-standard handling for it (since the standard is to just drop the value).
With linear types, the "close file" function you had to invoke will also return an error you have to handle.
This is a problem with many resource types (though maybe not all).
The function to close a database connection has to take in a linear value for a database handle, but it returns nil. How do you actually get rid of the handle? And how does the compiler stop you from doing it incorrectly (or does it?)?
---
Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program?
For example: you can define a record type that contains only free values, but tell the compiler you want it to be linear.
record Foo: Linear is
x: Int32; -- machine-sized ints are free
y: Int32; -- but `Foo` is declared to be linear
end;
let foo: Foo := Foo(x => 10, y => 20);
let { x: Int32, y: Int32 } := foo;
record File: Linear is
ptr: Pointer[Nat8];
end;
module Filesystem is
type File: Linear; -- `File` is opaque
-- etc.
end module.
module Filesystem is
type File: Linear;
function openFile(path: String): File;
function closeFile(file: File): Unit;
end module.
function closeFile(file: File): Unit is
let { ptr: Pointer[Nat8] } := file;
fclose(ptr); -- FFI-defined function
return nil;
end;
Borrowing allows you to relax the linearity constraints for some time: https://austral-lang.org/tutorial/borrowing
- we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it
- we can make a type opaque to importers of our module, which precludes direct destructuring by the user
- the compiler forces the user to eventually destroy the linear value
- therefore the user must call our cleanup function
And it's our responsibility to ensure the function implements the correct cleanup logic.
>we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it
I think I'll borrow this for the tutorial because it's very succinctly put.
I’m sure there’s a good answer. This is a really cool and impressive project.
EDIT: Ah, just got to the section on "The FFI Boundary". Makes sense!
Rust’s name shadowing is technically safe, but a massive footgun because humans are human and assume that in the same scope the same name refers to the same thing.
With name shadowing, you have to read through every line to make sure that the otherwise immutable value hasn’t been replaced with an impostor.
IMHO, it’s one of the worst Rust design decisions and shouldn’t be copied.
People will say they’re too lazy to come up with temporary variable names, meanwhile Rust doesn’t have multiple dispatch so every fn name has to be unique, which I personally find more irritating…
This is the painful approach, which is demonstrated in this very introductory document:
let f: File := openFile("test.txt");
let f1: File := writeString(f, "First line");
let f2: File := writeString(f1, "Another line");
...
> IMHO, it’s one of the worst Rust design decisions and shouldn’t be copied.
100% disagree. It's even more valuable to rust because of things like capture clause patterns.
> People will say they’re too lazy to come up with temporary variable names
No, people will say that most of the time temporary variable names make no sense and add no information. When you have an input of `T: AsRef<U>` and literally the first thing you do is ref' it, there's no value whatsoever to having two different names.
let f: File := openFile("filename.txt");
writeString(&!f, "first line");
writeString(&!f, "second line");
writeString(&!f, "third line");
closeFile(f);The unsafe pragma seems like an ugly exception to the otherwise seamless capability-safe design.
One thought— not a full one— is that a functional module system would allow for a comptime unsafe capability root.
I’m guessing the rejected alternative was to pass an unsafe capability; but that would get awkward quick…
Will there be partial application?
let appendHelloFile = appendFile("Hello");
let f = openFile("log.txt");
let f2 = appendHelloFile(f);
closeFile(f2);
Will there be a pipeline operator? I think this fits really nicely with linear types:
openFile("log.txt")
|> appendFile("Hello")
|> closeFile
You say that async will not be baked into the langauge. I think this is the right decision. However, will there be a syntatic sugar that can be used to avoid the "pyramid of doom" when writing promise-orientated code? It is possible to make this general purpose if done right.
I'd say the fact that these examples are around show that NxM, green-over-kernel threading works and works well. It made it through the crucible of fashion and is now a "good" way. Much like GC did. So I'd say your claim that kernel threads are it is misplaced... unless you just consider NxM threads to be kernel threads w/ some sugar?
BTW, you have a typo in one of your examples.
> import (
> ...,
> Relase_Filesystem,
> ...
> )
At a first glance, I only see advantages with this approach. What would be the caveats of using Austral instead of Rust (disregarding the ecosystem and toolchain factors)?
Is there a different mechanism for compile-time programming?
> A common misconception is that checking for allocation failure is pointless, since a program might be terminated by the OS if memory is exhausted, or because platforms that implement memory overcommit (such as Linux) will always return a pointer as though allocation had succeeded, and crash when writing to that pointer. This is a misconception for the following reasons:
> Memory overcommit on Linux can be turned off.
> Linux is not the only platform.
> Memory exhaustion is not the only situation where allocation might fail: if memory is sufficiently fragmented that a chunk of the requested size is not available, allocation will fail.
This is kind of the eternal vim vs eMacs debate but for malloc. In practice, I’ve not found this philosophy to be useful and actually problematic and the reasons given are the “easy” ones to convince more junior engineers. They’re true btw and the counter points provided aren’t really convincing. Regardless, the real reasons are:
* Memory allocation failures happen infrequently in practice.
* No one writes tests that simulate behavior of code under allocation failures.
* Memory allocation failures are basically treated as contract violations anyway in terms of triage - it’s not different from any other bug and you’d still need to fix it.
Crashing on a memory allocation failure:
* there’s no untested error recovery code to worry about
* the cause of the malloc failure means something else is broken / misconfigured. A crash tells you what to fix / when to fix it. A silent recovery attempt (when successful) will mask this and shift the problem (eg bug in error handling later or something)
There are times when you allocate memory and could handle failure gracefully by rejecting the request or something. However, as I mentioned. Memory allocation failures are rare and when they happen you need to fix a bug anyway. So crashing on a rare condition instead of running untested error recovery code is probably preferable in general.
Context: I have experience in mobile, embedded, desktop, and cloud so I’ve seen the gamut of dev environments. And everywhere the “abandon on malloc failure” turns out to be a more maintainable strategy that results in more robust code that’s simpler and shorter and faster/cheaper to develop because you’re not writing and thinking about error handling paths that never get run.
Regardless, it is kind of interesting to see a language adopt this philosophy. Maybe that can address some of the problems of trying to do this manually in other languages. I’m skeptical because the error paths problem remains, but I’m open to the experiment
If we consider instead filesystem space exhaustion, it's easier to imagine a reasonable expectation that the system could enter a degraded service state (e.g. reads work but writes don't), then recover without restart.
In fact I've worked on products that expected to provide exactly that kind of behavior, and we (tried to) test it.
So yes, some applications should handle a file system full failure. I’ve written code where the file system code was problematic (an infinite loop causing 100% cpu usage is common because it’s a daemon). I still will take that because it was caught so early in testing and we had a clear repro case to go after to reproduce the problem, fix it etc.
The other huge difference is that memory allocation is everywhere. Technically, everything should be passing a memory allocator if the function might allocate. After all, maybe I want my container to allocate the next set of nodes somewhere else or at the very least I want to use a pool allocator for some scope of code. In practice, this too is too much even though it’s infinitely more practical and useful than failable allocations.
TLDR: memory allocations are qualitatively different enough because it’s hidden global state that’s used everywhere. If you’re not going to have a memory allocator passed into every function as an override able parameter, faillable allocations aren’t practically interesting. This was a lesson learned about a decade ago but it seems like there’s pockets in the community that still disagree and push back against this. I wish them luck.
This is how Zig works.
> In practice, this too is too much even though it’s infinitely more practical and useful than failable allocations.
It seems to be working well enough for Zig.
Anyway, [1] shows the pros of this approach. But notice what’s not being discussed. This acknowledges that you have effectively increased the number of error paths in your program and you have to go through quite a bit of effort to get coverage to get some confidence of the behavior. Think of it in terms of ROI. Testing for malloc failures is comparatively expensive. It’s not logic based so you have to do it probabilistically and hope your test coverage works well and the issue happens infrequently (really never) in production. If it happens never, you’ve wasted all that test effort. If it happens very rarely, you’ve still wasted the effort because the probability that your test coverage accurately simulated the failure path is probably fairly low in a common path. It also sounds like zig’s allocator is actually quite dumb.
So while making sure to require explicit allocators, what’s a missed opportunity I think:
1. The default program allocator should be passed into main / dlinit. It’s not. This seems like a bad choice.
2. All malloc code in practice, I suspect, ends up getting propagated with try. That means you’re paying a performance cost for all the error checks that never get executed in practice (mostly in terms of icache pressure). Compare with rust where allocation failures typically panic and an optimized application will have panic set to abort leaving unwinding to a background process responsible for error reporting. That’s means there’s no stack unwinding and no error handling code for malloc failures without any change in safety guarantees.
Zig is a neat experiment and I understand why it’s proponents like it. I still would never choose it in production at this time:
1. The safety issues means that it’s not thaaat different in profile from C. It’s significantly easier to write safe code, but it’s not easier to audit / make guarantees.
2. Development speed is higher than some thing like Rust but when performance is a bit less critical higher level GC languages (Kotlin, Go etc) seem to make more sense.
So it’s hard to see what niche of professional development Zig can fill. Now being a hobbyist language is fine and it’s doing a lot of interesting things to show the ergonomics of other choices we wouldn’t otherwise see. But I would personally be very careful about making assumptions like “it seems to be working well enough for Zig” until it gets into the hands of a broader community. Things that seem to work OK earlier can shift drastically at scale.
[1] https://www.lagerdata.com/articles/testing-memory-allocation...
> > Memory overcommit on Linux can be turned off.
No, it can't in reality.
Nothing works in Linux when you turn of the overcommit as more or less every Linux lib and program relies on this behavior.
> However, as I mentioned. Memory allocation failures are rare and when they happen you need to fix a bug anyway. So crashing on a rare condition instead of running untested error recovery code is probably preferable in general.
That does not apply to safety critical code.
"Just crashing" a system in (for example) a nuclear power plant is not an option!
Or imagine, the controller of your car breaks crashes at some critical point in time and you can't break until the system rebooted.
Of course all code paths need to be tested. That's an obvious fact.
That’s one strategy. Another strategy is to run parallel controllers and using majority consensus. Distributed systems tells us that provides better guarantees but you have to design your system better instead of your code to avoid coupling (eg so that bad sensor data doesn’t take down multiple CPUs you need to basically duplicate a lot of your electronics). Safety critical systems should probably also be using formal proofs but that’s a secondary thing. However, on net that hardware duplication is probably a fraction of the cost and building your systems to reboot quickly in the face of the fault and testing fault handling regularly catches entires swathes of problems more simply and cheaply.
module body Test is
function recur(n: Nat64): Nat64 is
if n < 2 then
return n;
else
return recur(n - 1);
end if;
end;
function main(): ExitCode is
print("recur(50000000) = ");
printLn(recur(50000000));
return ExitSuccess();
end;
end module body.
I'm not impressed to be honest.
I would be less harsh if this wouldn't be advertised as sane and safe language. But it is.
---
¹ Of course you could fix this with for example trampolining. But than the promise of "no hidden control flow or functions calls or allocations" would be broken instantly.
That's not an implementation bug!
If you `recur` less often it works just fine.
Like I said, the language as such can't catch such bugs, as I see it.
Yes, I've mentioned this.
> […] it’s a limitation of your operating environment.
No, it isn't.
Memory is finite.
If your language doesn't handle this fact it's inherently unsafe, and a ticking time bomb.
> What else would you expect to happen?
Simply: No random crashes.
Especially as such a crash relies on the environment where the code is run. So it may work just fine "on your machine" but than crash in production…
That's imho a big no-no for anything that wants to be a "safe systems language" (especially as the post is mentioning things like nuclear power plants as target audience).
gcc -fwrapv generated.c -lm
To play devil's advocate: Why not stick with C as it seems to be the more "secure" language in this case? (Even we all know that C is inherently insecure, which is the reason for alternative system languages in the first place).
Trapping on overflow requires passing a flag to GCC. I didn't list that in the readme because there's like fifty other hardening flags like that and it would overcomplicate the presentation. I'll certainly add it to the build system, when it exists.