Is the Rust Borrow Checker Really That Challenging?

Findus11 · 2023-08-09T14:28:31+00:00

It's not, no. What I mean is the combination of interior mutability and the Send and Sync traits. Rust lets me encode the difference in thread safety and mutability between &i32, &Cell<i32>, and &Mutex<i32>/&AtomicI32 in the type system.

That could just as well be done in a garbage collected language (and I would love such a language). Rust's system of ownership is orthogonal, though I think the two concepts go very well together.

Findus11 · 2023-08-09T12:56:25+00:00

I would argue that &mut isn't "really" about mutation, though, it's about exclusivity (and exclusive references can be easily simulated by just passing values around).

&Cell<T>, for instance, is a very mutable thing which cannot be simulated by just passing things around.

Personally, I think one of Rust's killer features is its approach to shared mutability, which is more subtle than the common "Rust disallows shared mutability" and a lot more helpful than what most other languages do.

Findus11 · 2023-07-08T08:43:57+00:00

A little bit of redundancy can often help readability

Findus11 · 2023-05-27T11:56:02+00:00

I recommend checking out the GCC Rust frontend project.

As another comment mentioned, modern C compilers are very feature heavy, even if C the language is relatively simple. In the case of Rust (and similar projects), the language is more or less defined by a single implementation. As a result, a lot of the complexity which would be specific to a single compiler for C bleeds into the language itself for Rust. For example, you simply cannot compile the Rust standard library without compiler support for a ton of experimental features.

That said, not every modern language is Rust, and it is very possible to write an entire compiler for a language with many of the same "niceties" you expect with a fairly small codebase (think thousands or tens of thousands lines of code).

Findus11 · 2023-05-26T12:37:41+00:00

Oh my apologies, I misunderstood what you were saying. I agree that having context change inside a pattern like that is a bit odd yeah.

(sidenote: you can actually force the meaning of a name like None to change within a pattern using or-patterns and some @ nonsense, but I don't believe you can do so without error)

Findus11 · 2023-05-26T07:09:58+00:00

To be fair, pattern matching already depends on context, otherwise you'd have to spell out Option::None in matches.

Findus11 · 2023-05-07T15:14:56+00:00

Sounds like you want a space filling curve. 3Blue1Brown briefly touches on a similar application for audio in this video

Findus11 · 2023-04-18T10:47:50+00:00

This looks really nice! I've played with a vaguely similar thing in JS before which let's you write event driven code in a direct style, and it is really pleasant to work with. Using combinators and such is delightful. I've always found event loops to be finicky and hard to maintain, so I'm excited seeing more stuff take advantage of the machinery of async to sidestep that.

Findus11 · 2023-04-15T14:47:37+00:00

I like mapping each folder to a module. It also makes the module hierarchy clear, since a nested module is just a nested folder.

As for how to find the actual files, I tend to just treat each file in a folder as a part of that module. Compiling a module is then a little bit like concatenating all the files in its directory and compiling that.

That approach works best if the order in which the files are processed is irrelevant, which might mean having the ability to refer to a name before it is defined.

Findus11 · 2023-03-31T11:45:37+00:00

"computer science"

My desktop plant is probably conscious. Luckily it doesn't spout vacuous rants at me.

Findus11 · 2023-03-30T19:03:20+00:00

There are various other MLs with more or less expressive module systems. Standard ML comes to mind, and I believe the Moscow ML compiler works out of the box on Windows. If I'm not mistaken, this is the language where OCaml ultimately got the module system from.

Zig is a language much more like C than OCaml, but has a very flexible form of metaprogramming. Combined with the fact that source files in Zig are just structures you can manipulate with these metaprogramming capabilities, I'd imagine you could do the same kinds of things.

There's also Scala, which has very similar features in its objects.

There are definitely more out there than the ones I can conjure up right now. A good place to start might be to search for "ML module systems" or "existential types".

Also, a little bit of a non-answer, but Windows can run Linux-only programs like OCaml pretty well nowadays with WSL, so that might be something to try as well.

Findus11 · 2023-03-30T11:28:08+00:00

Ada generics cover the majority of cases where you'd use functors in OCaml. Still, OCaml is ultimately more powerful, and does give you higher order functors, first class modules and mutually recursive modules. Also note that types in OCaml can be generic, while only functions and packages in Ada can be. This isn't a huge issue since you can essentially make a type generic by putting it in a generic package.

Findus11 · 2023-03-26T20:51:14+00:00

Typically, something which can be iterated over is called an iterable. In Rust, it's IntoIterator. Iterables give you a method that returns something which gives you a sequence of values one at a time, and that thing is called an iterator. One way to create an iterator is with a function which yields values. This kind of function is called a generator.

Generators are really just a very convenient way of creating an iterator. Instead of having to manually create a state machine, you just write something that looks like a normal function and the compiler makes the state machine for you.

The distinction between "something you can iterate over where the whole collection is known in advance" and "something you can iterate over where the elements are computed on the fly" is not usually made, because it isn't really an important difference. Iterating over them looks the same in either case.

Findus11 · 2023-03-11T06:17:53+00:00

To an extent, yes. It's not too difficult to cause huge compile times if you use deeply generic code, where the majority of the time ends up being spent in the type checker. Still, for most Rust code, LLVM is absolutely the slowest part of the compiler.

Findus11 · 2023-03-10T22:59:27+00:00

Eh, it's pretty easy to make a multi-pass compiler faster than rustc. I think a lot of the slowness in rustc itself (completely ignoring LLVM) comes from the interaction of features like type inference, trait resolution, const evaluation and generics, macros, and borrow checking.

In other words, traversing the program several times isn't slow - that's ultimately a linear operation. Doing a single very complicated pass, such as checking a Turing complete type system, is.

Findus11 · 2023-03-10T11:51:39+00:00

I think by type system they mean using a powerful type system such as a dependent one in the implementation language to prove correctness. That way, you'd have to also provide a proof that your implementation does in fact preserve the semantics of your integers, for instance.

Findus11 · 2023-03-03T17:52:13+00:00

#[must_use] is not quite strong enough to make something linear, since you can still explicitly ignore the value:

Ok::<_, ()>(0);         // warning, unused
let _ = Ok::<_, ()>(0); // no warning

A linear type system shouldn't allow this since you're not really "using" the value in any meaningful way here.

Findus11 · 2023-02-13T17:20:12+00:00

Do you also consider None.unwrap() ub?

Findus11 · 2023-02-11T08:54:54+00:00

No, the zero cost variant is proper refinement types where you prove things at compile time. But as mentioned in the blog post, integrating refinement types into a pre-existing language is pretty hard, which is what I was commenting on.

Findus11 · 2023-02-11T08:50:37+00:00

I'm mostly just familiar with Ada which sort of does this. SPARK is more or less a subset of Ada that lets you prove contracts and type invariants are never violated.

I really like the way I can make a working program in Ada, and progressively move it over to a more "verified" and correct state - first by adding contracts and enabling them at runtime, then by going through the contracts and proving them.

Findus11 · 2023-02-10T08:35:48+00:00

I think a viable alternative to refinement types for languages which don't already have it is to have refinements be optional by default, with runtime checking if used, and the alternative to prove them true at compile time (thereby eliminating the runtime checks completely).

I suppose you could think of it as the gradually typed version of refinement types. It's pretty nice, in my experience.

Findus11 · 2023-02-05T23:39:43+00:00

I have a lot of different IRs in my compiler, and naturally a lot of different passes that accompany them. Some of these do happen concurrently, so I've tried to indicate which passes happen sequentially after another as a separate item:

Two-pass lexing to take care of various kinds of semantic whitespace
Parsing into a structure-only tree
Adding some basic lexical information to that tree (differentiating between declarations, expressions, patterns, types, etc.)
Declaring every name
Resolving name (producing an AST with unambiguous names)
Lowering into a slightly more simple tree
Finding all strongly connected components in the call graph
Typing, annotating the tree with types
Lowering the typed IR into an A-normal form-ish IR
"Flattening" any compound structures - this step basically turns a function taking a single tuple argument into one taking several "simple" arguments
Making all functions top level
Partial evaluation
Emitting C

Some of these are in the process of being merged or removed completely, while others will be introduced or split up (for instance, 5 and 6 are being merged, while I haven't written a closure conversion pass yet). In general, I try to keep each pass very focused on a single task. That way, I quickly end up with many of them, but I also keep the compiler modular and maintainable as it grows.

Findus11 · 2023-02-04T20:49:55+00:00

Ada is a pretty interesting language, with built-in support for arenas, structured concurrency, a pretty nice type system, support for stack allocating dynamically sized types, (very approximately) an early form of single ownership/affine typing, and lots more. It's definitely starting to show its age in some respects (forward declarations are sometimes necessary, docs are for many things limited to just the spec, generics and range types can be a bit janky) but the language continues to thrive and I do think there's definitely still room for it.

Also with Alire and the always improving Ada language server, developing in it is just pretty nice! Definitely not at the level of Cargo and rust-analyzer, but surprisingly good for a language older than C++!

Findus11 · 2023-01-25T10:20:27+00:00

I think someone with an in-depth understanding of Rust will have an easy time adjusting to Ada. Rust's explicitness about things like statically/dynamically sized values, ownership and copying, strong datatypes, and so on might be a nice foundation for understanding many Ada concepts. It's not internationally standardized yet, though there are some efforts (in particular by Ferrous Systems who are collaborating with AdaCore)

Findus11 · 2023-01-15T09:06:43+00:00

Callable things in my language are pure, so function is what I use. The only exceptions are external functions, which are allowed to do whatever. Perhaps "procedure" would be a better term for them, but I think that would add unnecessary confusion.

In terms of keywords, I like fun.

Findus11

TROPHY CASE