SabrinaJewson

4 ms·

1.
by SabrinaJewson 3d ago
In Rust, `loop {}` is an expression of type `!`, which means that from a type-theoretic perspective it is inhabited. This means that the Curry–Howard correspondence fails for Rust.
2.
by SabrinaJewson 4d ago
You’re going to hate when you learn that the never type is inhabited
3.
by SabrinaJewson 4d ago
Do you have an example of a piece of code that behaves in a surprising way because of this rule?
4.
by SabrinaJewson 4d ago
You’re using “subtype” in two distinct, but related, senses here, and I think this should be clarified. From a more category-theoretic perspective, a type A is a “subtype” of a type B when there is an embedding of A inside B. In this sense,
5.
by SabrinaJewson 4mo ago
As the creator of a library that lets you import Markdown into Typst directly in the Typst build process, without the use of external tools like Pandoc, I confess I find it this all a little inconvenient! It seems more advantageous to me to
6.
by SabrinaJewson 5mo ago
Related is the paper [What is a closed-form number?], which explores the field E, defined as the smallest subfield of ℂ closed under exp and log. I believe the set of numbers that can be generated using exp-minus-log is a strict subset of t
7.
by SabrinaJewson 6mo ago
How does that relate at all? Classical logic is not any less rigorous than other kinds of logic.
8.
by SabrinaJewson 6mo ago
I do not think this parallel works, because I think you would struggle to find a discipline for which this is not the case. It is trivial to enumerate all the possible scientific or historical hypothesis, or all the possible building bluepr
9.
by SabrinaJewson 7mo ago
In general in Rust, “length” refers to “count”. If you view strings as being sequences of Unicode scalar values, then it might seem odd that `str::len` counts bytes, but if you view strings as being a subset of byte slices it makes perfect
10.
by SabrinaJewson 7mo ago
You’re ignoring the obvious reason, aside from the network effect: there are no alternative solutions. Some people are building Discord alternatives but they are far from production-ready, often lacking critical features (e.g. Matrix not be
11.
by SabrinaJewson 10mo ago
You can claim that “learning disability” should mean whatever, but this does not change the fact that medical experts define “learning disability” such that they do not inherently impede intelligence: https://ehvi.org/learni
12.
by SabrinaJewson 10mo ago
You know that “learning disability” isn’t a synonym for “stupid”, right? We neither call people who are less academically able “disabled”, nor are disabled people necessarily less able to work academically (apart from some more debilitating
13.
by SabrinaJewson 10mo ago
I don’t know why you’re so angry at this statement, because it’s factually true. Do you truly believe that the proportion of families who stigmatize mental health care is negligible?
14.
by SabrinaJewson 10mo ago
100%. The school and the Internet are the two places children can encounter opinions different from their parents’ for the first time. With an increase in homeschooling and recent pushes to ban social media for children, it’s clear that cri
15.
by SabrinaJewson 10mo ago
This comment contains a lot of false information. I’m first going to point out that there is a model of Lean’s type theory called the cardinality model, in which all types of equal cardinality are modelled as the same set. This is why I say
16.
by SabrinaJewson 10mo ago
In type theory, all singleton types are isomorphic and have no useful distinguishing characteristics (indeed, this is true of all types of the same cardinality – and even then, comparing cardinalities is always undecidable and thus irreleva
17.
by SabrinaJewson 10mo ago
Well, Ladybird appears to be getting a headstart on having detractors.[0] [0]: https://drewdevault.com/2025/09/24/2025-09-24-Cloudflare-and...
18.
by SabrinaJewson 11mo ago
What about DEI makes it an “ideological” movement as opposed to other movements who are presumably not ideological? And I’m not sure what “most people”, is supposed to mean; you do realize you’re talking about 49% – that is, under half, so
19.
by SabrinaJewson 1y ago
Ferrocene is a specification but it’s not a formal specification. [Minirust]( https://github.com/minirust/minirust ) is the closest thing we have to a formal spec but it’s very much a work-in-progress.
20.
by SabrinaJewson 1y ago
“Natively” is important here because it’s actually relatively easy to get it working with a package: https://github.com/ntjess/wrap-it
21.
by SabrinaJewson 1y ago
English alternatives like “The staff enjoyed it later” or “The staff had the pleasure of eating it later” I would expect come across more euphemistic than normal to the average English-speaking viewer. So the question is whether the origina
22.
by SabrinaJewson 1y ago
No, because you only have to choose _one_ s for the proof to work, and a finite number of choices is valid in intuitionistic and constructive mathematics.
23.
by SabrinaJewson 1y ago
> Addressing your issue directly, the Axiom of Choice is actively debated: The axiom of choice is not required to prove Cantor’s theorem, that any set has strictly smaller cardinality than its powerset. Actually, I can recount the proof
24.
by SabrinaJewson 1y ago
> For example, the idea that there are the same number of integers as even integers is a stupid one that in the end does not lead anywhere useful. I am not sure what you are arguing here. We’ve been teaching this to all undergraduate mat
25.
by SabrinaJewson 1y ago
We can work with unnameable things very easily. Take, for instance, every known theorem that quantifies over all real numbers. If you try to argue that proving theorems about these real numbers does not constitute “working with” them, it se
26.
by SabrinaJewson 1y ago
I don’t know about you, I can work with it just fine. I know its properties. I can manipulate it. I can prove theorems about it. What more is there? In fact, if you are to argue that we cannot know a “raw” real number, I would point out tha
27.
by SabrinaJewson 1y ago
It’s less nice from a computational perspective. But almost no mathematicians care about computation – they care about semantics, and there is no sense in which Lean’s quotients are a hack from a semantic perspective. I’m sure it makes comp
28.
by SabrinaJewson 1y ago
You need some source of infinite-ness, otherwise the entire theory can be modelled by finite sets. It can be provided by the natural numbers or W types or inductive types, but the naturals are arguably the most fundamental of the three.
29.
by SabrinaJewson 1y ago
> Is there anything more primitive than the inductive data type? I believe that the natural numbers are more primitive than inductive data types, since all inductive data types may be constructed from the natural numbers alongside a smal
30.
by SabrinaJewson 1y ago
I’m not sure what you mean by “theorems remain the same”. If you take away induction from Peano arithmetic, you get Robinson arithmetic, which has many more models, including (from https://math.stackexchange.com/a/40765

More ›