#rustlang

[as-if-and-only-if]

Rust’s never type is wild to me.

So, if you’re not familiar with type theory, the empty type, which we’ll denote ∅ here (which Rust calls never, but more on that later) is the type with no elements.

But…how do you actually say that the type “has no elements” within the type theory?

You can’t say something like ¬∃x, x : ∅, in part because inside most type theories, this statement doesn’t even make sense: we need to know the type of x when bound, and more importantly, typing judgments like x : ∅ are not statements you can make within the theory itself.

Actually, you often don’t even want to use ¬ at all: we want to define ¬P in terms of ∅ as P → ∅ ! This is because having an element of the empty type would (if all goes well) be a contradiction, so if you can construct such a contradiction out of P (i.e. ->), then P must be false. ∅ is near the foundations, so we don’t have much to work with when setting up its meaning.

What we can do is encode the principle of explosion, i.e. that given an element of the empty type (a contradiction!) we can derive anything.

That is, we have an axiom explode : ∀(A : Type), ∅ → A. For any type A, give me an element x of ∅, and I will hand you an element of that type (namely explode A x : A).

(If you’re familiar, ignore universe polymorphism/Type vs. Prop and the fact that A isn’t a type family.)

This is what makes the empty type the empty type. If we didn’t include this axiom, the empty type would have no real emptiness behavior besides “gee, I can’t quite figure out how to make an element of this type”. You wouldn’t know it’s empty, since there would be no consequences to finding out that something has type ∅.

(Aside: this axiom fits into a very general pattern of what it means to define a type inductively, and lets us do “induction on the empty type”. It’s not ad-hoc!)

———

So it should be clear that if you ever do find an element of ∅, your theory is inconsistent, as you can prove anything you want.

Which is why Rust’s empty type, called never, is pretty neat. To me, someone who does not know Rust, and who literally opened the docs as soon as I installed them, scrolled down, and said “ooh, what’s never?”

See, Rust expressions can have type never. (I’m calling them expressions; I don’t know if this is what rustaceans call them)

But, how?! Surely that breaks everything! Well…yes. Which is why the only way to maintain consistency is to have these expressions break everything.

Let me explain: the things with type never never return a value (hence the name). They diverge: they’re things like exit or break or infinite loops.

And thanks to the explode axiom, these expressions can be coerced to any type. For example, you can say x: u32 = { exit() }, and Rust will say “makes sense to me”. (Apologies for any bad Rust syntax.)

This is—surprisingly!—fine.

exit() : never, just like any element of the empty type, really is a contradiction in the type system, but being able to write it in Rust code doesn’t actually make the type system inconsistent—since we leave the type system as soon as it’s encountered. (Or, in the case of an infinite loop, we never manage to actually finish constructing a value of never.)

So, while the syntax of Rust can contain “contradictions”, they never get the chance to behave as contradictions in the model of Rust’s type system formed by the values it constructs at runtime. I.e. running a real program never invalidates the type system. We’re saved from the runtime nonsense that would be created by explode A x by having the system actually explode instead.

There’s something to be said for this, but it is weird. Saying “x : u32” in Rust is apparently scoped in a certain way: it says “as long as the value we call x exists, it has type u32.” It doesn’t guarantee the existence of something with type u32.

This means that you don’t actually have to break the whole type system to use never; you just have to break the context in which x exists. E.g., if you’re inside a function, then let x: bool { return 500 }, where the return returns to the outer function, is fine. x never finishes being constructed, so the guarantee provided by its type annotation is (vacuously) satisfied.

I wonder if this is linked to the notion of lifetimes in Rust, and how that’s reflected in the theory behind the type system. And I’m not a type theorist (or someone who knows Rust), but I am also curious how type theorists talk about diverging terms; in Lean, for example, a top-level term of type Empty is verboten. You create diverging terms by using the partial keyword, and then you’re prohibited from proving anything about their behavior (but they still have types as usual).

This isn’t the first time people have talked about this, by far, I’m sure; happy to hear any takes (or corrections). Much to learn! :)

[forever-stuck-on-java-8]

shout out to @fish-shell for completing their port to @rust-official

[itsjunetime]

I made a little terminal-based PDF viewer! For fun, mostly, 'cause I thought it would be a fun challenge, but also a PDF viewer is the only other windowed program I currently use on my computer besides my browser and my terminal, so I thought it would be fun to replace.

It could still be more performant and handle its multi-threading stuff better (and I do have some ideas to do that), but I thought people here might get a kick out of this. It's built in rust, using ratatui, etc, you know the deal.

If you want to check it out, the code's here: https://github.com/itsjunetime/tdf

[daniel-nerd]

got myself some thigh high socks that means my code will compile now! right?

[quietmarie]

bwaaaa I'm doing programming crimes again

(this is from a small project that is heavily inspired by axum, but don't worry it won't go anywhere I realised there are better approaches)

[zephiris]

Java is a trash language that should burn in the parts of hell where hitler is

Rust on the other hand is a bratty lil language that should burn in the parts of hell where queers party

[somerandev]

🫚 Day 35 of Game Dev for 🫱Teleport Man🫲

When the right hand is occupied, the left one punches instead of using the teleport ability.

Tried making the punch push objects... but...... i t h i n k i m e s s e d s o m e t h i n g u p

[bizarre-furry-bastard]

[youboirusty]

If your language doesn't have a yeet keyword what are you doing with your life

[voltradar]

Got my tights, skirt, heart choker, and hoodie. Anything else needed to complie my Rust?

[aeriavelocity]

Rust is DOOM Eternal

Rust makes you want to learn functional programming just by the fact that variables are immutable by default - and if you want to pass a mutable variable through a function, good luck.

You have to declare "&mut variable" in not only the function call, but also the damn function signature.

Compare that to Python where variables can't even be immutable.

Of course - this is probably a good thing. I'm a devotee of functional programming myself, so I'm biased, but to be fair, I didn't even know what functional programming WAS before I learned Rust.

If C is the Dark Souls of programming, Rust is the DOOM Eternal. (and Python is the Garry's Mod)

[agapi-kalyptei]

Not gonna lie. I wrote my first programs 34 years ago but I never was a "real" developer in the sense that I'd write fast desktop apps, manage threads, and all that low level stuff. So learning Rust in the past few months, even if I have some very basic experience with programming in assembly, is still a lot to digest. However, today I got back to my test project and am really hyped that I have.... a button that increments a number.

"Ha, I can do that in javascript in 10 minutes." I mean yeah. Obviously. Anyone can. Here's the cool thing tho. I made mine overly complicated.

The UI looks as you'd expect it to, mostly a starter project leftovers:

The HTML is as simple as can be, just plain HTML and javascript, no compile step. We live in stone ages here and we love it.

The submit button has a simple handler in javascript:

This is, once again, trivial, and all just from the template project. Bottom part says "when a user clicks this button, call "greet" function". The top part is the greet function that invokes a Tauri command also called "greet".

What's Tauri? An open source project that lets you write JS/TS/Rust applications with WebView and bundle them as stand-alone, self-contained, one-file applications for desktop, and starting with Tauri 2.0 (now in beta.2) also for Android (and later iOS). If you know Electron (Slack, Spotify, Discord etc all use Electron, they're just websites with Chromium and C++ code packaged around them).

Anyway. Tauri runs a Rust "server" application that serves your HTML/JS app, but also lets you run high-performance Rust code. Adding a command is relatively simple:

Here's where things get interesting. For me.

Because I wanted to learn Bevy, a game engine written in Rust, because I want to learn how to write using a high-performance functional-programming-like pattern called ECS (Entity Component System), I have added Bevy to this project.

However, both Tauri and Bevy block on the main thread, so I had to find a tutorial on how to spawn Bevy in a different thread, and how to pass information to it. An example:

#[tauri::command] turns a normal function into a Tauri command that I can call from HTML/JS. It injects resource called BevyBridge which is just two lines of code: #[derive(Resource)] pub struct BevyBridge(pub Sender<u64>, pub Receiver<;u64>);

Sender and Receiver being from crossbeam-channel bevy crate which is for sending data back and forth safely and quickly between individual threads.

so "state.0.send(1)" means I'm sending a 64-bit unsigned integer with a value 1 to the channel.

And this is how to receive the message - inside of Bevy engine, in a separate thread. For simplicity, if I send zero, it resets the counter, and if I send any number it adds 100000 to the number, just for clarity. (Elsewhere I'm incrementing it by 1 on every game loop, so theoretically 60x a second. Or 15000x a second because Bevy is unreasonably fast and it doesn't need to render anything in this setup.)

And the best part is that with a single command (cargo tauri build) I get an .msi file, an .exe installer, both around 4MB, and a 11MB .exe file with no dependencies besides WebView (installed on every current desktop OS by default). There's just something about giving someone a floppy disk with an executable that you made yourself.

Is it dumb? Yes. Does it make me happy? No. Does it make me glad, and very relieved that I'm not completely lost? You bet.

[suntreehq]

Learning Rust and using my Visuals app to get some autumn vibes. (Video sped up by 1.25x).

I was hoping bombarding my subconscious mind with autumnal images would help me deal with the change of season. But I get enough autumnal vibes just looking out the window so maybe I will change it up to sunny imagery.

[itsjunetime]

i built a little crate for tower-based rust web servers the other day, if anyone’s interested. it’s called tower-no-ai, and it adds a layer to your server which can redirect all “AI” scraping bots to a URL of your choice (such as a 10gb file that hetzner uses for speed testing - see below). here’s how you can use it:

it also provides a function to serve a robots.txt file which will disallow all of these same bots from scraping your site (but obviously, it’s up to these bots to respect your robots.txt, which is why the redirect layer is more recommended). because it’s built for tower, it should work with all crates which support tower (such as axum, warp, tonic, etc.). there’s also an option to add a pseudo-random query parameter to the end of each redirect respond so that these bots (probably) won’t automatically cache the response of the url you redirect them to and instead just re-fetch it every time (to maximize time/resource wasting of these shitty bots).

you can view (and star, if you would so like :)) the repo here:

[habble0]

[forever-stuck-on-java-8]

hot take: most of the programs you guys are writing don't actually need the performance of rust. 80% of the time you can write the same application in a less complicated language in less time.

I say this because Operations has started a betting ring for how long cargo build takes for a rust web app that we inherited from an acquisition. Today it took 18 minutes.