ralfj

6 ms·

31.
by ralfj 1y ago
The long answer to this question can be found in https://research.ralfj.de/thesis.html . :)
32.
by ralfj 1y ago
> Rust allows different forms of contraction, which affine logic strictly prohibits. That's just wrong. Affine logic totally can have contraction for some propositions. Also, CH totally exists for non-dependently-typed languages -
33.
by ralfj 1y ago
I brought up Curry-Howard to explain why I am using an SO post about "affine logic" to make an argument about the definition of "affine language". Both are defined the same way: no (universal) contraction. That claim is
34.
by ralfj 1y ago
> multiple immutable shared references are a form of contraction No, they are not. You're not using a value more than once, you are borrowing it, which is an extension of affine logic but keeps true to the core principles of affin
35.
by ralfj 1y ago
> The aliasing rules of Rust for mutable references are different and more difficult than strict aliasing in C and C++. "more difficult" is a subjective statement. Can you substantiate that claim? I think there are indications
36.
by ralfj 1y ago
OTOH we have https://web.ist.utl.pt/nuno.lopes/pubs/ub-pldi25.pdf which shows that on a range of benchmarks, disabling all provenance-based reasoning (no strict aliasing, no "derived from" reasoning, onl
37.
by ralfj 1y ago
Pointer aliasing information is often crucial for vectorization. So in that sense TB is a big boost for vectorization. Also, note that the paper discussed here is about the model / language specification that defines the envelope of wh
38.
by ralfj 1y ago
Yeah, concurrency bugs that only occur in very specific situations are hard to track down with a pure testing tool. However, we have some ongoing work that should make Miri a lot better at this... we are just not sure yet whether we can get
39.
by ralfj 1y ago
C has an opt-out that works sometimes, if a compatible type exists. Rust has an opt-out that works always: use raw pointers (or interior mutable shared references) for all accesses, and you can stop worrying about aliasing altogether.
40.
by ralfj 1y ago
Thank you for your kind words. :)
41.
by ralfj 1y ago
> Well, the rust type system certainly does support contraction, as I can use a reference multiple times. So what is that if not contraction? It seems like rust at least does support contraction for references. Good question! For shared
42.
by ralfj 1y ago
I would say it is perfectly accurate to call Rust's type system affine. At its core, "affine" means that the type system has exchange and weakening but not contraction, and that exactly characterizes Rust's type system.
43.
by ralfj 1y ago
I would agree that C's strict aliasing rules are terrible. The rules we are proposing for Rust are very different. They are both more useful for compilers and, in my opinion, less onerous for programmers. We also have an actual in-lang
44.
by ralfj 1y ago
Thanks :-)
45.
by ralfj 1y ago
> allows more while still being provably safe. Note that we have not yet proven this. :) I hope to one day prove that every program accepted by the borrow checker is compatible with TB, but right now, that is only a (very well-tested) c
46.
by ralfj 1y ago
> Using pointers to coexist multiple mutable references to the same variable is undefined behavior. Yes, but which exact rule does it violate? What is the exact definition that says that it is UB? Tree Borrows is a proposal for exactly s
47.
by ralfj 2y ago
Good point, I do indeed use Flatseal. I added it to the blog post.
48.
by ralfj 2y ago
shrug all I know is I fixed some issues with compose sequences by giving flatpak apps access to XCompose. It may be something with electron apps not properly using ibus?
49.
by ralfj 3y ago
It's not just per-object. When you consider things like `restrict` pointers in C, and the aliasing model in Rust (e.g. Stacked Borrows), you have provenance distinctions even within a single allocated object.
50.
by ralfj 4y ago
I think you're suffering from over-optimism. ;) So far no language not designed for it has demonstrated that adopting a borrow-checker to interesting real-world use-cases is possible. The C++ project (C++ Core Guidelines it is called I
51.
by ralfj 4y ago
Beware of reading the library sources though, they can change any time without warning. Only the docs are guarantees that remain stable as Rust gets updated.
52.
by ralfj 4y ago
It is certainly possible to soundly reason about them. The C standard just does not describe how to do it. There is plenty of PL work (in particular everything considering ML with imperative features, many decades worth of work) where ref
53.
by ralfj 4y ago
I don't have a good way to include the image anyway (or I am too lazy to figure out how to do that in Jekyll, I guess), so its appearance(s) on my blog will be text-only for now. Thus no image license trouble. ;)
54.
by ralfj 4y ago
Which podcast was that? A Rust podcast with the main Zig dev sounds very interesting!
55.
by ralfj 4y ago
From a quick scroll, that seems to be just C-style `select` with `if` guards? What I was referring to is things like `match x { Some(y) => ..., None => ... }`, where there is data that is available only in some variants of the type (l
56.
by ralfj 4y ago
Oh that's interesting, I kept saying Apple is the only "big tech" company not using Rust. (Huawei should probably also be considered "big tech", but they are also using Rust.) But with Apple being as closed as the
57.
by ralfj 4y ago
Yeah, I use Firefox and I worry about the web increasingly becoming Chrome-only. :(
58.
by ralfj 4y ago
UCG and their Zulip are a good place for thorny "is this UB" questions, yeah. We're thin on documentation indeed. First need to figure out all the rules, then find enough people to write all the educational material to teach
59.
by ralfj 4y ago
My goal is that we can actually run it, but that would still only be useful for the following things: - Testing the spec itself - Ensuring that a more production-grade interpreter like Miri has the same semantics as the spec it claims to im
60.
by ralfj 4y ago
I used "Rust-style enums" because if I just say "enum" then people think I mean something else. ;) And then I added the clarification to make sure nobody thinks I would claim that Rust invented Rust-style enums. If I ju

More ›