I’ve always disagreed with “the language should make everything explicit.” It freezes you at one layer of abstraction, the one chosen by the designer. (And I don’t believe the “you can look at code and tell what assembly it emits” part. Not even C has that. If it were true, the optimizer would be too hamstrung to be any use.)
Making you type in destructors manually seems like a bad idea. If it’s too hard to tell when destructors are being called, couldn’t you have a tool or IDE annotate the code for you?
if you’re reaching for cyclic data at the application-level, you’re probably looking to model relations, in which case just use (a linear handle to) a relational database.
So once you need to go anywhere past the only-one-reference limit, you end up entirely outside the language where it can’t help you at all anymore. (Plus you’ve just incurred several orders of magnitude of performance overhead.)
I do agree it’s super cool that experimental languages are so easy to create now! Even if I don’t like all the resulting languages.
if you’re reaching for cyclic data at the application-level, you’re probably looking to model relations, in which case just use (a linear handle to) a relational database.
So once you need to go anywhere past the only-one-reference limit, you end up entirely outside the language where it can’t help you at all anymore. (Plus you’ve just incurred several orders of magnitude of performance overhead.)
In the original quote I linked to a post on modeling Relations in Cell. I knew that this sentence might draw some discussion, so let me expand on this point a little.
Relations don’t have to be modeled using a relational database; I used this example because it is one that ties into linear types. There are a lot of ways to model relations: through encapsulated state with a correct public interface, through applying data-oriented design principles, to reify relations, through another level of indirection by use of arenas, and so on. Some of these techniques are pretty fast, so modeling relations doesn’t necessarily incur a huge performance overhead. Indeed, the language Cell supports modeling relations in the language itself. I think languages should think more about handling relations, not less. Most real-world data is relational in nature.
When modeling free-form relational data at the application level, in the context of a long-running system, it makes no sense to roll your own subset of a relational database, except in a few exceptional cases where the performance is needed (e.g. game) or the relations being modeled are unlikely to change (e.g. compiler). If using relations to express some internal transformation more efficiently, by all means, skip the network hit and reify your relations at the library level.
Cell is very interesting! I had its website open in a tab for months and kept reading bits of it and thinking about the ideas. (I was working on a b-tree storage manager at the time and would muse about how to add relational features without introducing a whole query language.)
So yes, I totally agree about language support for relations. But that would require a third category of type, right? Value types, Linear types and Relations.
I find it weird to consider C a language that makes everything explicit since when you call a function in C that function can pretty much do whatever it wants to your entire universe. That seems like the opposite of explicit. But maybe calling opaque functions is not a consideration in this discussion.
Well, if everything were that explicit we’d just be writing state diagrams for Turing machines or something. It’s hard to write real code without subroutine calls!
The explicitness here is that C models the way you call subroutines with PUSH/POP and JSR/RET instructions in assembly.
I’ve always disagreed with “the language should make everything explicit.”
I don’t like it either, but there are definitely communities of people who like C, and who like Zig. There’s a demand for this sort of language, I think.
It freezes you at one layer of abstraction, the one chosen by the designer.
Exactly. This is a feature, if you are the sort of person who doesn’t like abstraction, because it gets in the way of understanding what is happening during execution.
And I don’t believe the “you can look at code and tell what assembly it emits” part.
I think this is a slogan that doesn’t fully capture the requirement. You have a simple language with a corresponding simple model of program execution, “at the layer of abstraction chosen by the designer”. And you can use this model to understand what a program will do by reading the code and executing it in your head, with all of the actions explicit, nothing hidden behind pesky abstractions.
Making you type in destructors manually seems like a bad idea.
Or, with different requirements, it may seem like an excellent idea. Destructors have side effects (freeing memory, closing files, etc). If destructors are implicit, you can’t see the order in which side effects occur by reading the code. In this version of reality, all side effects should be explicit in code.
if you’re reaching for cyclic data at the application-level, you’re probably looking to model relations, in which case just use (a linear handle to) a relational database.
So once you need to go anywhere past the only-one-reference limit, you end up entirely outside the language where it can’t help you at all anymore. (Plus you’ve just incurred several orders of magnitude of performance overhead.)
I don’t agree that you use a relational database in this case. You use an Entity/Component architecture and Data Oriented Programming. Done correctly, this provides better performance than object-oriented programming using a graph of objects connected by pointers. For example, the Zig compiler was recently rewritten in this style, for significantly improved performance. I read some of the code, and it was educational, because it’s faster code than anything I would write in one of my preferred programming languages.
For example, the Zig compiler was recently rewritten in this style, for significantly improved performance. I read some of the code, and it was educational,
Do you have a suggestion what to read or some other link?
For “how it works”, zig’s AST would be a good case study. The source is quite readable, as it’s self contained and independent of the rest of the compiler
If you can express linear types in less code than a garbage collector, why not just use linear types to manage memory?
Because a garbage collector results in a language that is much simpler to use and much more expressive? (It also has limitations, of course, for example there are resources other than memory that benefit from a more precise ownership discipline at the language level.)
I’d like to apologize for this rhetorical question, because comparing linear types and garbage collectors is a bit like comparing apples and oranges. I mean sure, they can both be used to model memory, but garbage collectors also deal with cycles, call destructors automatically, and so on.
What I do like about Linear/Affine types is that they provide exact fine-grained tracking of the lifecycle of each object, with zero runtime overhead. In Python, a GC’d language, you can end up with problems like async tasks being dropped by the garbage collector because you forgot to store a handle to them. This is something simply not possible in Linear languages.
To some degree, there’s a fundamental difference between a systems language and a scripting language. I love Python, and when I’m scripting, the last thing I care about is resources. I think that part of advancing programming as a discipline is realizing that there are different tools for different jobs. And while I wouldn’t add linear types to a scripting language, if writing a statically typed language in the future, linear/affine types seem like a great solution to deterministically managing memory.
Personally I think of garbage collection as a generally fine approach for handling memory, but not for handling other notions of resources that cannot be duplicated or forgotten at will – usually one end of a communication channel (file descriptor, sockets, database connections, etc.). I think that the distinction matters because it encourages us to think of language designs that let us handle memory in a convenient, low-effort way by default and resources in a higher-effort ownership-tracking way by default. Such a language would also let you model memory as resources when you really want to (rarely), or let you forget resources away using finalizers when you really want to (also rarely).
This sounds quite interesting, though I’m suspicious of linear types, since most times I’ve heard them discussed in practical languages it ends up with people calling them over-restrictive. I’m curious to see how Austral deals with graphs, caches and other messy data structures.
From looking at the github:
“No destructors” is a bold take, I wonder what lead to that decision?
“No global state”, sounds like you’ll have fun interfacing with hardware that is literally implemented as global state.
Looks like the syntax and module system takes a lot of my least favorite things about Ada. :/ Separate interface and implementation files, end if and end case to make refactoring as tedious as possible,
No type inference, also a bold take
On the whole, it feels… a little iffy. Kinda the evil twin of Go. Still, I should play around with it and see how it goes.
“No destructors” means that destructor functions are not called implicitly, like in C++ or Rust. Instead, destructors must be called explicitly, but the type system makes it safe. You can’t forget to call a destructor, and you can’t accidently call a destructor twice. This is more verbose than Rust, but follows from the design requirement “no implicit function calls”. Zig has a similar design requirement. And C is like this.
“No global state” is a very cool property, which I interpret as “no shared mutable state”. Obviously you need state to interact with the OS. The trick is to encapsulate all global state in capabilities which must be passed as arguments, and now you have capability based security, among other useful properties. I’ve been trying to figure out how to make that work in an Austral-adjacent language I’m designing. Austral claims to have “no global state”, but it’s … not designed and implemented yet? The spec says “The entrypoint function of an Austral program takes a single value of type RootCapability”. By contrast, the “hello world” example program is
module body Hello is
function main(): ExitCode is
printLn("Hello, world!");
return ExitSuccess();
end;
end module body.
Contrary to the spec, the main function doesn’t take a RootCapability argument. The printLn function doesn’t take a capability argument: it just encapsulates global state, like printf in C. There is no capability based interface to the OS to be seen here. Also, Austral has a C FFI, which contradicts the “no global state” property.
So it’s definitely a work in progress.
Digging further, here is experimental syntax (not finalized) for what Hello could look like if coded correctly using capabilities and “no global state”.
module body HelloWorld is
function main(root: RootCapability): ExitCode is
let termcap: TerminalCapability := acquireTermCap(&!root);
printLn(&termcap, "Hello, world!");
surrenderTermCap(termcap);
surrenderRoot(root);
return ExitSuccess();
end;
end module body.
You can’t forget to call a destructor, and you can’t accidently call a destructor twice.
Engage grumpy language designer mode… If the computer can catch the problem for me, and there’s only really one valid solution to it (call the destructor at the end of the scope), I’d really prefer the computer do it for me. IMO it’s no different from having to write end module body. when end alone is 100% unambiguous. While I am perfectly happy with the compiler forcing me to prove I know what I’m doing when there can be doubt of this fact, I would really prefer it to not actively waste my time. </grump>
The capability model is pretty cool, but IMO it suffers a lot from the Haskell IO Monad Problem, as lots of Rust code does from time to time as well. If you discover 5000 lines into your program that you want a function 10 deep in the call stack to log some info, then you have to change the function signatures for every intermediate function to take your TerminalCapability object as an argument as well. This is why people keep playing with the idea of context objects or implicit arguments, to ease the accounting burden by, again, telling the compiler to handle some of it for you. So I like the idea but the ergonomics are currently something of an unsolved problem. Will be interesting to see what they come up with, and how terrible it becomes to use in practice.
I basically agree with you, and my guess is that the ergonomics of Austral will likely be terrible, as a consequence of the language design requirements (no type inference, capabilities, linear logic, no implicit calls).
I don’t personally want to code in Austral, but one role I can see for a language like this is as a kind of safe portable assembly language, like WebAssembly but with very strong compile time security and safety guarantees, that can be verified quickly, in linear time, by a simple compiler. It’s nice if your security and safety properties can be guaranteed by a small core which is easy to audit. I dunno what ergonomic language compiles into Austral; that’s a research project.
The capability model is pretty cool, but IMO it suffers a lot from the Haskell IO Monad Problem […] If you discover 5000 lines into your program that you want a function 10 deep in the call stack to log some info, then you have to change the function signatures for every intermediate function […]
If you have rigidly-defined capability interfaces, then yes, this is a complete and total hassle. One thing I think improves ergonomics is effect inference, commonly found in languages with Algebraic Effects, like Koka. If you change the effects of a function 10 levels deep in the callstack, this effect type will be propogated up through the type signatures all functions calling that function. If you want to limit effects at a given point, like before calling library code, you can declare an explicit signature.
I know you’ve thought a lot about inference and context due to your work on Garnet (really enjoyed The Generics Problem); making everything explicit is likely to have horrible ergonomics. I think Austral would be well-suited to a project like a kernel, where everything should be readable and verifiable at the expense of ease of expression.
For this reason, despite being much more ergonomic, I think effect inference is at odds with Austral because of Austral’s need for everything to be explicit. (E.g. Austral limits type inference, why should it infer effects?) Exceptions were rejected in the language because they don’t mesh well with linear types; algebraic effects are ‘just’ an extension of exceptions (delimited continuations don’t play well with resources, I’d imagine). I don’t think Austral is the perfect language, but it does demonstrate a few patterns and a depth of consideration that I wish other projects gave to the task at hand.
If you change the effects of a function 10 levels deep in the callstack, this effect type will be propogated up through the type signatures all functions calling that function. If you want to limit effects at a given point, like before calling library code, you can declare an explicit signature.
That’s a pretty nice thought, and is sooooooomething like what I want to do with Garnet’s properties. The flip side of this idea is that these effects then become part of a function’s API, sneakily and silently, it then becomes super easy to make API-breaking changes without realizing. To make up an example, I could see a PRNG impl that does not allocate memory and gets used inside a function explicitly marked with the “no allocation” property, and if that impl gets changed to allocate memory for some reason then it will make distant code fail to compile. The API contract is still there, just implicit. It’s tricky; the best ideas I’ve had on helping with that thus far are an automated “semver sanitizer” program to make sure you haven’t done this by accident when releasing new software, and a linter or documentation generator capable of conjuring forth the full explicit effect signature of a particular function on demand. Those would let you at least debug the problem effectively when it occurs.
And yeah, I can argue with Austral about the decisions it makes, but from what I’ve seen so far those decisions are made deliberately. I just think a lot of those decisions make life harder than it needs to be. It’s a tradeoff they’re free to make of course, it just seems to go wayyyyyyy over to one edge of the balance. Still, that makes it an interesting case study for what that looks like, so I wish them well.
Austral is obviously a well-researched language written by someone who “gets” language design. I will add one thing: using OCaml is a huge reason this compiler is so simple. It is simply a pleasure to write compilers in OCaml, and it’s crazy what can be done in such a small amount of code.
My favorite example of this is the PLZoo. All of these are very small, stripped down languages, but a larger lang like Austral is really not far off from what’s going on in these example languages.
I think we hit a lull for a few years where theory and language technology just couldn’t keep up with industry. I do agree with the post here that this seems to be balancing recently, because we’re able to cherry-pick the theory of the last 30 or so years into what’s practically relevant for our day jobs. Linear types definitely fall in that camp, and I’m also excited to see what else shakes out in the next few years along these lines.
I work in the space that the author considers Austral’s potential niche (safety critical embedded). In my experience, almost everything in this space is still written in C or C++, with a small Ada/SPARK contingent as well. I would be thrilled to use something other than C++. The amount of work and effort that goes in to ensuring our C++ code is safe is enormous, and would almost completely vanish if we used a language like Rust or Austral that statically verifies certain safety properties.
However, it’s not quite that simple. There are a lot of factors involved when certifying safety critical software in aviation (the industry I am in). There is a reason C and C++ are still used so heavily, and it’s not because anyone believes these are languages well suited for safety critical applications, but rather because there is a large amount of already qualified tooling and processes for C and C++ that don’t yet exist for other languages. The agencies that perform the certification are also already familiar with C/C++. Using a different language (e.g. Rust) is not impossible, but would require a large engineering effort to create (and qualify) the necessary tools and processes for certification. The process would also take longer, as the certifiers are not as familiar with the language. So any organization that would even consider using something other than C/C++ faces a long (and expensive) uphill battle. There are efforts to standardize a formal specification for using Rust in some safety critical applications (IIRC just automotive for now), so there is some progress, but it’s a slow and long process.
I mention this because, as I said, I would love to see Austral (or similar) gain traction in this space, but that will likely not happen any time soon. I would be thrilled to be wrong about this though.
Yeah one of the things that struck me in my brushes with flight-certified software is how horrifically expensive it is. Releasing a bugfix update to already-good software can cost six figures USD. A large part of it is exactly because the languages and tooling are so obtuse, there’s an immense amount of manual work involved in reviewing and verifying everything. But I also believe better tools will only incrementally reduce that burden, you probably won’t get a 10x reduction in effort without some theoretical advance that lets you fundamentally rethink the process.
I’ve always disagreed with “the language should make everything explicit.” It freezes you at one layer of abstraction, the one chosen by the designer. (And I don’t believe the “you can look at code and tell what assembly it emits” part. Not even C has that. If it were true, the optimizer would be too hamstrung to be any use.)
Making you type in destructors manually seems like a bad idea. If it’s too hard to tell when destructors are being called, couldn’t you have a tool or IDE annotate the code for you?
So once you need to go anywhere past the only-one-reference limit, you end up entirely outside the language where it can’t help you at all anymore. (Plus you’ve just incurred several orders of magnitude of performance overhead.)
I do agree it’s super cool that experimental languages are so easy to create now! Even if I don’t like all the resulting languages.
In the original quote I linked to a post on modeling Relations in Cell. I knew that this sentence might draw some discussion, so let me expand on this point a little.
Relations don’t have to be modeled using a relational database; I used this example because it is one that ties into linear types. There are a lot of ways to model relations: through encapsulated state with a correct public interface, through applying data-oriented design principles, to reify relations, through another level of indirection by use of arenas, and so on. Some of these techniques are pretty fast, so modeling relations doesn’t necessarily incur a huge performance overhead. Indeed, the language Cell supports modeling relations in the language itself. I think languages should think more about handling relations, not less. Most real-world data is relational in nature.
When modeling free-form relational data at the application level, in the context of a long-running system, it makes no sense to roll your own subset of a relational database, except in a few exceptional cases where the performance is needed (e.g. game) or the relations being modeled are unlikely to change (e.g. compiler). If using relations to express some internal transformation more efficiently, by all means, skip the network hit and reify your relations at the library level.
Cell is very interesting! I had its website open in a tab for months and kept reading bits of it and thinking about the ideas. (I was working on a b-tree storage manager at the time and would muse about how to add relational features without introducing a whole query language.)
So yes, I totally agree about language support for relations. But that would require a third category of type, right? Value types, Linear types and Relations.
I find it weird to consider C a language that makes everything explicit since when you call a function in C that function can pretty much do whatever it wants to your entire universe. That seems like the opposite of explicit. But maybe calling opaque functions is not a consideration in this discussion.
Well, if everything were that explicit we’d just be writing state diagrams for Turing machines or something. It’s hard to write real code without subroutine calls!
The explicitness here is that C models the way you call subroutines with PUSH/POP and JSR/RET instructions in assembly.
I don’t like it either, but there are definitely communities of people who like C, and who like Zig. There’s a demand for this sort of language, I think.
Exactly. This is a feature, if you are the sort of person who doesn’t like abstraction, because it gets in the way of understanding what is happening during execution.
I think this is a slogan that doesn’t fully capture the requirement. You have a simple language with a corresponding simple model of program execution, “at the layer of abstraction chosen by the designer”. And you can use this model to understand what a program will do by reading the code and executing it in your head, with all of the actions explicit, nothing hidden behind pesky abstractions.
Or, with different requirements, it may seem like an excellent idea. Destructors have side effects (freeing memory, closing files, etc). If destructors are implicit, you can’t see the order in which side effects occur by reading the code. In this version of reality, all side effects should be explicit in code.
I don’t agree that you use a relational database in this case. You use an Entity/Component architecture and Data Oriented Programming. Done correctly, this provides better performance than object-oriented programming using a graph of objects connected by pointers. For example, the Zig compiler was recently rewritten in this style, for significantly improved performance. I read some of the code, and it was educational, because it’s faster code than anything I would write in one of my preferred programming languages.
Do you have a suggestion what to read or some other link?
If you enjoy watching talks, here’s one I did on this topic: A Practical Guide to Applying Data-Oriented Design
For “how it works”, zig’s AST would be a good case study. The source is quite readable, as it’s self contained and independent of the rest of the compiler
There’s also a great explainer post:
This is a good overview of the architecture of the new self-hosted Zig compiler: https://mitchellh.com/zig
Because a garbage collector results in a language that is much simpler to use and much more expressive? (It also has limitations, of course, for example there are resources other than memory that benefit from a more precise ownership discipline at the language level.)
I’d like to apologize for this rhetorical question, because comparing linear types and garbage collectors is a bit like comparing apples and oranges. I mean sure, they can both be used to model memory, but garbage collectors also deal with cycles, call destructors automatically, and so on.
What I do like about Linear/Affine types is that they provide exact fine-grained tracking of the lifecycle of each object, with zero runtime overhead. In Python, a GC’d language, you can end up with problems like async tasks being dropped by the garbage collector because you forgot to store a handle to them. This is something simply not possible in Linear languages.
To some degree, there’s a fundamental difference between a systems language and a scripting language. I love Python, and when I’m scripting, the last thing I care about is resources. I think that part of advancing programming as a discipline is realizing that there are different tools for different jobs. And while I wouldn’t add linear types to a scripting language, if writing a statically typed language in the future, linear/affine types seem like a great solution to deterministically managing memory.
Personally I think of garbage collection as a generally fine approach for handling memory, but not for handling other notions of resources that cannot be duplicated or forgotten at will – usually one end of a communication channel (file descriptor, sockets, database connections, etc.). I think that the distinction matters because it encourages us to think of language designs that let us handle memory in a convenient, low-effort way by default and resources in a higher-effort ownership-tracking way by default. Such a language would also let you model memory as resources when you really want to (rarely), or let you forget resources away using finalizers when you really want to (also rarely).
This sounds quite interesting, though I’m suspicious of linear types, since most times I’ve heard them discussed in practical languages it ends up with people calling them over-restrictive. I’m curious to see how Austral deals with graphs, caches and other messy data structures.
From looking at the github:
end ifandend caseto make refactoring as tedious as possible,On the whole, it feels… a little iffy. Kinda the evil twin of Go. Still, I should play around with it and see how it goes.
“No destructors” means that destructor functions are not called implicitly, like in C++ or Rust. Instead, destructors must be called explicitly, but the type system makes it safe. You can’t forget to call a destructor, and you can’t accidently call a destructor twice. This is more verbose than Rust, but follows from the design requirement “no implicit function calls”. Zig has a similar design requirement. And C is like this.
“No global state” is a very cool property, which I interpret as “no shared mutable state”. Obviously you need state to interact with the OS. The trick is to encapsulate all global state in capabilities which must be passed as arguments, and now you have capability based security, among other useful properties. I’ve been trying to figure out how to make that work in an Austral-adjacent language I’m designing. Austral claims to have “no global state”, but it’s … not designed and implemented yet? The spec says “The entrypoint function of an Austral program takes a single value of type RootCapability”. By contrast, the “hello world” example program is
Contrary to the spec, the
mainfunction doesn’t take a RootCapability argument. TheprintLnfunction doesn’t take a capability argument: it just encapsulates global state, likeprintfin C. There is no capability based interface to the OS to be seen here. Also, Austral has a C FFI, which contradicts the “no global state” property.So it’s definitely a work in progress.
Digging further, here is experimental syntax (not finalized) for what Hello could look like if coded correctly using capabilities and “no global state”.
https://github.com/austral/austral/issues/336
Engage grumpy language designer mode… If the computer can catch the problem for me, and there’s only really one valid solution to it (call the destructor at the end of the scope), I’d really prefer the computer do it for me. IMO it’s no different from having to write
end module body.whenendalone is 100% unambiguous. While I am perfectly happy with the compiler forcing me to prove I know what I’m doing when there can be doubt of this fact, I would really prefer it to not actively waste my time. </grump>The capability model is pretty cool, but IMO it suffers a lot from the Haskell IO Monad Problem, as lots of Rust code does from time to time as well. If you discover 5000 lines into your program that you want a function 10 deep in the call stack to log some info, then you have to change the function signatures for every intermediate function to take your
TerminalCapabilityobject as an argument as well. This is why people keep playing with the idea of context objects or implicit arguments, to ease the accounting burden by, again, telling the compiler to handle some of it for you. So I like the idea but the ergonomics are currently something of an unsolved problem. Will be interesting to see what they come up with, and how terrible it becomes to use in practice.I basically agree with you, and my guess is that the ergonomics of Austral will likely be terrible, as a consequence of the language design requirements (no type inference, capabilities, linear logic, no implicit calls).
I don’t personally want to code in Austral, but one role I can see for a language like this is as a kind of safe portable assembly language, like WebAssembly but with very strong compile time security and safety guarantees, that can be verified quickly, in linear time, by a simple compiler. It’s nice if your security and safety properties can be guaranteed by a small core which is easy to audit. I dunno what ergonomic language compiles into Austral; that’s a research project.
If you have rigidly-defined capability interfaces, then yes, this is a complete and total hassle. One thing I think improves ergonomics is effect inference, commonly found in languages with Algebraic Effects, like Koka. If you change the effects of a function 10 levels deep in the callstack, this effect type will be propogated up through the type signatures all functions calling that function. If you want to limit effects at a given point, like before calling library code, you can declare an explicit signature.
I know you’ve thought a lot about inference and context due to your work on Garnet (really enjoyed The Generics Problem); making everything explicit is likely to have horrible ergonomics. I think Austral would be well-suited to a project like a kernel, where everything should be readable and verifiable at the expense of ease of expression.
For this reason, despite being much more ergonomic, I think effect inference is at odds with Austral because of Austral’s need for everything to be explicit. (E.g. Austral limits type inference, why should it infer effects?) Exceptions were rejected in the language because they don’t mesh well with linear types; algebraic effects are ‘just’ an extension of exceptions (delimited continuations don’t play well with resources, I’d imagine). I don’t think Austral is the perfect language, but it does demonstrate a few patterns and a depth of consideration that I wish other projects gave to the task at hand.
Aww, thank you!
That’s a pretty nice thought, and is sooooooomething like what I want to do with Garnet’s properties. The flip side of this idea is that these effects then become part of a function’s API, sneakily and silently, it then becomes super easy to make API-breaking changes without realizing. To make up an example, I could see a PRNG impl that does not allocate memory and gets used inside a function explicitly marked with the “no allocation” property, and if that impl gets changed to allocate memory for some reason then it will make distant code fail to compile. The API contract is still there, just implicit. It’s tricky; the best ideas I’ve had on helping with that thus far are an automated “semver sanitizer” program to make sure you haven’t done this by accident when releasing new software, and a linter or documentation generator capable of conjuring forth the full explicit effect signature of a particular function on demand. Those would let you at least debug the problem effectively when it occurs.
And yeah, I can argue with Austral about the decisions it makes, but from what I’ve seen so far those decisions are made deliberately. I just think a lot of those decisions make life harder than it needs to be. It’s a tradeoff they’re free to make of course, it just seems to go wayyyyyyy over to one edge of the balance. Still, that makes it an interesting case study for what that looks like, so I wish them well.
Would it make sense to disallow inference of public functions’ signatures? Would that be enough to prevent effect inference from causing this problem?
Austral is obviously a well-researched language written by someone who “gets” language design. I will add one thing: using OCaml is a huge reason this compiler is so simple. It is simply a pleasure to write compilers in OCaml, and it’s crazy what can be done in such a small amount of code.
My favorite example of this is the PLZoo. All of these are very small, stripped down languages, but a larger lang like Austral is really not far off from what’s going on in these example languages.
I think we hit a lull for a few years where theory and language technology just couldn’t keep up with industry. I do agree with the post here that this seems to be balancing recently, because we’re able to cherry-pick the theory of the last 30 or so years into what’s practically relevant for our day jobs. Linear types definitely fall in that camp, and I’m also excited to see what else shakes out in the next few years along these lines.
I work in the space that the author considers Austral’s potential niche (safety critical embedded). In my experience, almost everything in this space is still written in C or C++, with a small Ada/SPARK contingent as well. I would be thrilled to use something other than C++. The amount of work and effort that goes in to ensuring our C++ code is safe is enormous, and would almost completely vanish if we used a language like Rust or Austral that statically verifies certain safety properties.
However, it’s not quite that simple. There are a lot of factors involved when certifying safety critical software in aviation (the industry I am in). There is a reason C and C++ are still used so heavily, and it’s not because anyone believes these are languages well suited for safety critical applications, but rather because there is a large amount of already qualified tooling and processes for C and C++ that don’t yet exist for other languages. The agencies that perform the certification are also already familiar with C/C++. Using a different language (e.g. Rust) is not impossible, but would require a large engineering effort to create (and qualify) the necessary tools and processes for certification. The process would also take longer, as the certifiers are not as familiar with the language. So any organization that would even consider using something other than C/C++ faces a long (and expensive) uphill battle. There are efforts to standardize a formal specification for using Rust in some safety critical applications (IIRC just automotive for now), so there is some progress, but it’s a slow and long process.
I mention this because, as I said, I would love to see Austral (or similar) gain traction in this space, but that will likely not happen any time soon. I would be thrilled to be wrong about this though.
Yeah one of the things that struck me in my brushes with flight-certified software is how horrifically expensive it is. Releasing a bugfix update to already-good software can cost six figures USD. A large part of it is exactly because the languages and tooling are so obtuse, there’s an immense amount of manual work involved in reviewing and verifying everything. But I also believe better tools will only incrementally reduce that burden, you probably won’t get a 10x reduction in effort without some theoretical advance that lets you fundamentally rethink the process.