This is incorrect. The set paradox it’s analogous to is the inability to make the set of all ordinals. Russel’s paradox is the inability to make the set of all sets.
Technically speaking, because it's not a set, we should say it involves the collection of all sets that don't contain themselves. But then, who's asking...
This is the easiest of the paradoxes mentioned in this thread to explain. I want to emphasize that this proof uses the technique of "Assume P, derive contradiction, therefore not P". This kind of proof relies on knowing what the running assumptions are at the time that the contradiction is derived, so I'm going to try to make that explicit.
Here's our first assumption: suppose that there's a set X with the property that for any set Y, Y is a member of X if and only if Y doesn't contain itself as a member. In other words, suppose that the collection of sets that don't contain themselves is a set and call it X.
Here's another assumption: Suppose X contains itself. Then by the premise, X doesn't contain itself, which is contradictory. Since the innermost assumption is that X contains itself, this proves that X doesn't contain itself (under the other assumption).
But if X doesn't contain itself, then by the premise again, X is in X, which is again contradictory. Now the only remaining assumption is that X exists, and so this proves that there cannot be a set with the stated property. In other words, the collection of all sets that don't contain themselves is not a set.
Let R = {X \notin X}, i.e. all sets that do not contain themselves. Now is R \in R? Well this is the case if and only if R \notin R. But this clearly cannot be.
Like the barber that shaves all men not shaving themselves.
The paradox. If you create a set theory in which that set exists, you get a paradox and a contradiction. So the usual "fix" is to disallow that from being a set (because it is "too big"), and then you can form a theory which is consistent as far as we know.
Perhaps I overstated how related the two were. I was pulling mostly from the Lean documentation on Universes [0]
> The formal argument for this is known as Girard's Paradox. It is related to a better-known paradox known as Russell's Paradox, which was used to show that early versions of set theory were inconsistent. In these set theories, a set can be defined by a property.
I came across this when wondering if there were any efforts to give programmers additional information via audio, similar to how colors are used in syntax highlighting.
There are some interested experiments out there in modes of highlighting, such as where colors are assigned to particular variables.
IMO syntax highlighting is still the best default for navigation and general reading, but I can imagine tasks where I might want to temporarily toggle what information I'm getting through that color-of-text route.
The final comments in this text seem sobering and indicate an openness to change. I worked recently on a project to migrate RediSearch to Rust, and this was partially motivated by a decent number of recent CVEs. If SQLite doesn't have this problem, then there needs to be some other strong argument for moving to Rust.
I also think it's important to have really solid understandings (which can take a few decades I imagine) to understand the bounds of what Rust is good at. For example, I personally think it's unclear how good Rust can be for GUI applications.
It's nice that they don't dismiss out-of-hand the idea of using a language other than C (the conclusion is far less dogmatic than the editorialized title here suggests (the actual title of the page being "Why Is SQLite Coded In C?")). But let's be clear that the stability and "boringness" that C currently enjoys took literal decades to realize (pre-ANSI C was a wild-west shitshow that makes pre-ECMA Javascript look tame by comparison), and giving the same leeway to other languages probably doesn't suggest using e.g. Rust until at least 2040 or so.
It carries some weight, very roughly in the direction of formal verification. Since (assuming there isn't any unsafe), a specific class of bugs are guaranteed to not happen.
However, this repo seems like it uses quite a bit of unsafe, by their own admission.
You never have only one requirement to satisfy. For example, if you'd welcome a certain amount of contributors, your language should be something people know or people like to learn. And of course it may just be the mood of the initiator, which I find completely fine.
Personally I find rust projects very inviting. Figuring out the amount of unsafe code is easy with grep/rg (to a certain degree), the project structure is pretty standardized, etc. All of this makes even a complex project relatively easy to start with. At the same time, the language is pretty usual (C-like and readable). I understand people like it, and writing "written in rust" is a good call for those people, I guess.
"Written in JS" would communicate something else than "written in D" or "written in C++". It communicates a lot of things implicitly.
This idea about communicating size/alignment is actually something we're doing on the port of RediSearch to Rust [0]. We have an "opaque sized type" which is declared on the Rust-side, and has its size & alignment communicated to the C-side via cbindgen. The C-side has no visibility into the fields, but it can still allocate it on the stack.
It's a bit ugly due to cbindgen not supporting const-generic expressions and macro-expansion being nightly-only. It seems like this will be a generally useful mechanism to be able to use values which are not traditionally FFI-safe across FFI boundaries.
It's kind of an exploratory phase for what works sensibly with Rust's borrow checker, especially since most UI libraries/frameworks really rely on a GC.
reply