It’s more like adding a runtime handle to the struct.
Modulo that I’m not sure any langage with a sync/async split has an “async” runtime built entirely out of sync operations. So a library can’t take a runtime for a caller and get whatever implementation the caller decided to use.
> I’m not sure any langage with a sync/async split has an “async” runtime built entirely out of sync operations.
You get into hairy problems of definition, but you can definitely create an "async" runtime out of "sync" operations: implement an async runtime with calls to C. C doesn't have a concept of "async", and more or less all async runtime end up like this.
I've implemented Future (Rust) on a struct for a Windows operation based only on C calls into the OS. The struct maintains everything needed to know the state of the IO, and while I coupled the impl to the runtime for efficiency (I've written it too), it's not strictly necessary from memory.
> You get into hairy problems of definition, but you can definitely create an "async" runtime out of "sync" operations: implement an async runtime with calls to C. C doesn't have a concept of "async", and more or less all async runtime end up like this.
While C doesn't have async OS generally provide APIs which are non-blocking, and that is what async runtimes are implemented on top of.
By sync operations I mean implementing an "async" runtime entirely atop blocking operations, without bouncing them through any sort of worker threads or anything.
From my perspective, not having to deal with strings is one of the big benefits, but I believe the main argument is actually that it trivializes alpha equivalence.
As for renaming, if you're going to be looking at every binding anyway, changing most of them is no big deal (unless of course that entails doing many deep copies)
I used De Bruijn indices when attempting to prove correctness of a toy language of mine. It's an elegant solution, but I found them exceedingly difficult to reason about both intuitively and in proofs. That being said, I've yet to find a better system (that isn't just augmenting De Bruijn indices) for implementing any sort of lambda calculus.
Lean is more complex to develop in than most programming languages since it relies heavily on interactive programming, i.e. the context pane. The "easy way" is with a plugin.
If you're interested in learning more about Lean for writing proofs, I would recommend The Mechanics of Proof [0]. It strips out a lot of the convenience tactics in Mathlib to focus on the more primitive mechanisms Mathlib builds on.
I've seen the book, but I've personally found it not very useful for a person who wants to first get the basics.
The natural number's game is actually quite fun, and I did understand much better the language. And it's also interactive, so you can try your solutions, and there are hints when stuck.
On linux, I'd want it to be dictated by my DE or WM. I have Super+shift+q set to close windows on my machine, so I wouldn't be crazy about software adding its own keybind to do the same.
Even when it worked, QC itself is not massively deployable right now. Agencies will be sucking their thumbs while everyone migrates to something stronger or even quantum-proof algorithms. No drama.
- fractional scaling is a known sore spot, but it seems like it's getting better fast. Wayland finally has fractional scaling and the upcoming release of KDE is coming with proper fractional scaling support.
- The laptop sleep setting is some that can be (sometimes) fixed by changing a bios setting (called something along the lines of 'Sleep State'). It's part of a Microsoft + Intel initiative to make PCs "more like smartphones," with all the extra "user friendliness" you would expect from that.
