Viewing profile — SabrinaJewson

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 al…

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 …

How does that relate at all? Classical logic is not any less rigorous than other kinds of logic.

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 o…

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 vie…

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 productio…

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 …

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 …

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 negligibl…

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 …

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…

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, com…

Well, Ladybird appears to be getting a headstart on having detractors.[0] [0]: https://drewdevault.com/2025/09/24/2025-09-24-Cloudflare-and...

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…

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 muc…

“Natively” is important here because it’s actually relatively easy to get it working with a package: https://github.com/ntjess/wrap-it

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 Eng…

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.

> 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 cardinal…

> 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 arguin…

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…

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 th…

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 ar…

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 …

> 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…