This article, everything else aside, is excellent. I wrote a rambling bunch of stuff in this comment and before I posted I had to cut out a lot, because HN comments aren’t really the best place for an in depth discussion about type theory implementations. So, I’m just going to read the compiler source and then get a hold of you later.
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.
This is fantastically written documentation. What is even more exciting for me, that this is almost exactly what I was dreaming and talking non-stop about for the last few years. I never figured out the brilliant insight about redundancy of operator precedence. On the more embarrassing note in numerous implementation not-quite-attempts I always ended up gutting loops as a feature in favor of recursion and went with effects for capabilities (among other things). Then I was usually caught off guard by either of those or my other darling — partial application interacting in unexpected way (only for me probably) with linear types, which always punched me back to square one. Extremely impressed with how sound and grounded in reality your choices are. Fantastic job.
Fuck, I mean… yeah. Thanks for one more insight, by showing me that sending message/calling a method is a binary operation, seems so obvious but I never made that connection. This day started by shelling by Russian rockets, but reading the post and your comment somehow made it… good?
I always get caught off-guard by how much baby we’ve thrown with the water with modern languages compared to some brilliancy we had in Lisp and Smalltalk. Both are extremely out of my cup of tea region, but I learn so much when I interact with them. The only thing JS and something like Java taught me is to stay away:)
> Thanks for one more insight, by showing me that sending message/calling a method is a binary operation
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
binds as
(((foo bar) - baz) / qux) qux: quux
You can still get into sticky situations, mostly thanks to the cascading operator ";":
a b; c
sends the message following ";" to the receiver of the message preceding ";". So here it's equivalent to
a b.
a c
now consider:
foo + bar qux; quux
This is equivalent to
foo + bar qux.
foo quux
Because the message which precedes the ";" is actually "+", whose receiver is "foo":
All Smalltalk history talks mention that APL was a major influence, and it didn't have operator precedence either. In addition, the Smalltalk-72 scheme of "parse as you go" would make implementing precedence really awkward.
Smalltalk-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.
Seems interesting though I can not say that I like the Ada inheritance (especially the interface files, but the verbosity as well, the lack of tuples and verbosity of Pair seems like it would quickly be frustrating with a linear type system, as well as the seeming lack of same-scope shadowing).
Shame the examples are a bit too simplistic to show the value of linearity e.g.
function closeFile(file: File): Unit;
that's the wrong interface, because closing a file can error. And it is an issue with destructors, which linear types can solve.
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).
>that's the wrong interface, because closing a file can error
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).
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).
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.
No, on the contrary: you can recover from destructor failure by returning error values, as in Haskell or Rust.
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];
Where returning a `File` means closing it failed. Then you can try again, or abort. And returning `Unit` means closing succeeded. You can bikeshed the exact return type endlessly.
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.
And here we are. A language "focused on safety and correctness" where you need to argue because error handling is neglected instead of being put front, and not even the most trivial resource management is thought out (even big sounding terms like "linear types" and "capabilities" were thrown on the table).
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.
> A language "focused on safety and correctness" where you need to argue because error handling is neglected instead of being put front, and not even the most trivial resource management is thought out (even big sounding terms like "linear types" and "capabilities" were thrown on the table).
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.
Presumably close should return either success or a broken_file of some sort. I can't think of a use case for getting back a file which looks like you can write to it when close failed previously.
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.
> Realistically, it shouldn't, and there's no way you would be able to handle it properly even if it did.
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 like this a lot! For several years I've been pondering the exact same idea of using linear types this way, combined with some kind of Rust-style borrowing. I've never really had any serious ambitions to create a programming language, though, so I'm happy to see someone finally doing this for real.
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.
^ this. there's a lot i like from Austral, but I think I disagree on some fundamental level with the "simplicity" goal. I simply don't think it is necessarily conductive to less errors, and expressivity of a language matters. There is a balance to be found.
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
Agree separating the interface and implementation is not a great idea. It seems like a decision that's designed to waste time (in copying definitions from one place to another, in compilation errors).
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).
It's a good start. I expect that a lot will be learned by implementing the standard library, particularly if a serious attempt is made to make it work well on multiple platforms. Do you want to model a lot of platform-specific restrictions like Rust or sweep them under the rug like Go?
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.
You probably don't want all the platform-specific stuff in a capability based language, because the filesystems in mainstream OSs are not capability based, and you can't sugar-coat a non-capability system with capabilities. The capabilities need to be built in, and one of the main principles behind them is that you should not separate designation and authority. Access-control-lists (MAC, DAC, RBAC, etc) violate this principle - the authority is held separately from the designator, and this is why these systems are always vulnerable to confused deputies.
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).
Yes. It seems like running a capability-based system on top of a non-capability-based filesystem is a form of sandboxing. It's not impossible - for example, it's how filesystem API's work in a browser. But it's tricky to prevent sandbox escapes.
Simple spec? Check. Linear type memory management? Check. Ada syntax? Check. Avoiding footguns? Check. It's like you took my fantasy of the ideal low level programming language that I've never gotten around to implementing, and you actually built it.
This is rather interesting. Safe and reliable programming in the large is an important goal. Generics, sum types and typeclasses make different kinds of useful abstraction available from the get-go. I'm looking forward to progress on this.
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".
I think this is entirely down to the mentality of the developer. Feedback that the project will achieve traction and user adoption is motivating for many of us.
Yes but "I'm looking forward to seeing more" is about as reliable an indicator of future adoption as "For sure I'll invest in your company" is, coming from friends and family.
If it motivates you, you're in for disappointment.
I'd love to have the time. Family and work take it almost all up. Compilers, semantic models and type systems are of high interest for me and I've done some work related to those. But I'd be out of my depth. There are many more areas that could be contributed to. Hats off if he wrote the docs as well as the compiler, it's great technical writing, as an example of another area that usually needs assitance.
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.
Can somebody explain what is "linear" about linear types. There seems to be a common pattern in computer science of reusing well established mathematical terms (e.g. vectors, tensors) in confusing ways.
It comes from Linear Logic, where there's no inference A&B->A. I think the point of the name is "there's always progress".
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
This is my first type hearing about linear types, but my guess is the name comes from the fact that you have to repeatedly “thread” a value through your code to keep using it. If you look at the example for Files, you have to pass the outputted file pointer from writeFile as an input value to the next writeFile. So you can picture that one file pointer as linearly threading through you code. And it’s specifically linear because your “thread” can’t “branch”, because that would mean you’re using the same value twice (except an if-statement is kind of a branch, but it’s ok because when the code runs the value will follow a linear path).
But I agree that “linear types” is not a great name. Something like “single use types” would be clearer to me.
> Girard himself, in his native language (cf. Girard, Cours de Logique I, Hermann, 2006, Section 1.B.2), writes:
> "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.
Linear in the sense you can draw a line, not a tree, through the usage - in terms of memory allocation, the linear item cannot be copied (ie create an allocation), or destroyed during its lifetime. The naming comes from linear logic.
It comes from linear logic and that's as far as I know.
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.
My understanding is that the 'linear' terminology derives from the field of Linear Logic[1]. But, I am by no means an expert on theoretical computer science etymology!
This is not correct actually. It comes from linear logic, and it's connection to ordinary linear functions we all learned in school is clear if you think about it: any linear function f(x) can be written in a form where x appears only once on the right hand side, ie. f(x) = Bx + C.
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.
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.
A linear type is an annotation on another thing to opt into semantics checking. The linear file probably has an integer file handle hidden insider it.
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.
> 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.
Interesting ideas but I'm in the camp that having everything be explicit causes complexity to be foisted on the user. There are times and places where that simplicity might offer some advantages but I'd rather my systems language scale between contexts.
> be explicit causes complexity to be foisted on the user
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...
> having everything be explicit causes complexity to be foisted on the user
I agree. I think once you understand and trust a language-provided abstraction or automation, you can use it happily. It's a machine you don't need to see the entrails of.
> I'd rather my systems language scale between contexts.
I appreciate when they work well as a general purpose language.
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.
What does/will Austral do on out of stack memory? Assuming it maps tail calls to branches, the call stack still grows on the non-tail calls.
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.
Nice writeup. I think Rust will also get true linear types at some point (i.e. types that can't be auto-dropped) because they're required for improved async support. 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. The author is surely aware of this, but it's worth making it clear.
>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.
> So linear types are incompatible with traditional exception handling.
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;" ..
Instead of linear types, would it be possible to just enforce some kind of "must call close" policy?
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?
>1. Does that solve the close problem as well as linear types?
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.
> No, because if pointers are copyable, multiple places can point to the same memory address, and all destructor guarantees are gone.
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?
>This seems orthogonal to me. If you allow pointers, then linear types don't help you either, right?
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:
>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]
If `List` is linear then this can use in place reversal while the interface is referentially transparent. Because for the type system, the list that goes in is consumed, and cannot be used again, and the list that comes out is a brand new linear type. It just happens to use the same storage.
There are uses for unsafe pointers beyond FFI. In fact, it's only feasible to prove that unsafe pointers are used soundly if the unsafety is contained within a well-defined program module. (Proper inter-module 'FFI' with unsafe pointers would need something like full separation logic, which is very complicated!)
"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."
Even when you could verify this, it wouldn't prevent use after free bugs.
Agreed. To be clear, I'm not explaining why the OP chose linear types over affine types (I have mixed feelings on choosing one or the other) but rather why one needs either affine or linear types rather than "disposed exactly once" types.
> 1. Does that solve the close problem as well as linear types?
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).
Can you give some examples of what it looks like to destroy a linear value? Elsewhere in the thread you said the compiler doesn't privilege destructor functions over anything else. I'm a bit confused how it works.
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?
The idea is: linear interface, free core. Free types are the opposite of linear: they're unrestricted and can be used any number of types.
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;
Then instances of `Foo` behave like any other linear type. To destroy it, you'd destructure its contents:
let foo: Foo := Foo(x => 10, y => 20);
let { x: Int32, y: Int32 } := foo;
So, how does this relate to safety? Because you can have something like:
record File: Linear is
ptr: Pointer[Nat8];
end;
Where `File` is a linear record that contains a free (unsafe) file pointer. You can hide this behind an API, as an opaque type:
module Filesystem is
type File: Linear; -- `File` is opaque
-- etc.
end module.
Opaque types can be imported from the outside, but clients don't know what they contain. So they can't construct them directly or destructure them or access record fields. Instead, you have to expose constructors and destructors in the API:
module Filesystem is
type File: Linear;
function openFile(path: String): File;
function closeFile(file: File): Unit;
end module.
The implementation of `closeFile` would simply be:
function closeFile(file: File): Unit is
let { ptr: Pointer[Nat8] } := file;
fclose(ptr); -- FFI-defined function
return nil;
end;
>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?
Trying to understand: what’s to prevent someone from calling an FFI-defined function on a free type without going through the whole linear types rigmarole? E.g. could I call `fopen` and `fclose` directly to circumvent the whole `File` interface?
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!
I like that in rust one can reuse variable names, since they are dead anyway. Makes sense to ‘update’ the old name with the new value, sort of like a swap-and-kill. Does austral have this? Seems like no reason not to.
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");
...
Foo63 is one of those things I do not miss from Erlang.
> 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.
This may be at odds with the no operator precedence rule.
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.
Interesting design. I agree 99% with the choices. My only disagreement would be about not being able to overload binary operators. I wonder how the type system handles the inherent overloading of * for floats and integers. Besides this minor point, I totally agree with the design and intent!
> 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).
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?
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)?
Thanks. Actually I read that one too. Several mentions of Region but not really a definition that i could find. Not that it’s a big deal, just curious. I infer some similarity with Rust’a lifetimes but I’m a bit hazy on those
Interesting observation that contradicts my experience:
> 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
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 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.
Can't disagree, but still it feels wrong, doesn't it?
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.
If you enter file system exhaustion (or a read only file system), most applications should fail similarly. You want to be very very careful to only add error handling for known failure modes you know, expect, have seen in production, and have test coverage for. Everything else should fail as gracefully as possible. Anything else is “safety theater” where you feel better but it’s totally illusory.
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.
Zig is still relatively immature so it’s hard to judge just quite what software patterns will look like at scale, especially when it leaves the niche of language enthusiasts using it to build stuff.
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.
The language was trivial to break in a few minutes. (And it likely can't do anything about it [edit to make this clear: This is not an implementation bug. Without depended types or abstract interpretation this is unfixable¹, as I see it]).
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.
This code generates almost 3.5 kLOC of C which results in a segmentation fault when compiled and run on my machine.
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.
This is a bit harsh. It’s still early in the language’s development, and the quality of the compiler/generated code shouldn’t be conflated with the principles of the language itself.
Uh, that one is an implementation bug. It's presumably compiling the call to recur as a normal C call. It should either be a goto (or loop, w/e) or use the musttail compiler extension.
> […] 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).
I've used the flags given in the readme on GitHub.
gcc -fwrapv generated.c -lm
But anyway (besides that this is a lazy answer as it sounds like "not my problem"), how could a C compiler prevent this in the general case?
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.
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.