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 all a little inconvenient!

It seems more advantageous to me to have only one build step and no intermediary files. We don’t support all the exotic features of Pandoc Markdown, but support much more customization in other areas.

The library: https://github.com/SabrinaJewson/cmarker.typ

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 this.

In a similar vein to this post, the paper points out that general polynomials do not have solutions in E, so of course exp-minus-log is similarly incomplete.

What is intriguing is that we don’t even know whether many simple equations like exp(-x) = x (i.e. the [omega constant]) have solutions in E. We of course suspect they don’t, but this conjecture is not proven: https://en.wikipedia.org/wiki/Schanuel%27s_conjecture

What is a closed-form number?: http://timothychow.net/closedform.pdf omega constant: https://en.wikipedia.org/wiki/Omega_constant

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 or historical hypothesis, or all the possible building blueprints, or all the possible programs, or all the possible recipes, or legal arguments…

The fact that the domain of study is countable and computable is obvious because humans can’t really study uncountable or uncomputable things. The process of doing anything at all can always be thought of as narrowing down a large space, but this doesn’t provide more insight than the view that it’s building things up.

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 sense that it gives the number of UTF-8 code units (and it is analoguous to, say, how Javascript uses `.length` to return the number of UTF-16 code units). So I think it depends on perspective.

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 being able to delete rooms, or still having trouble with decrypting messages). It is simply the case at this point in time that Discord is factually the least bad option for many many use cases.

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/learning-vs-intellectual-disabilities/. This isn’t my definition, it’s the definition used by medical experts. A quote from that article:

Learning disabilities don’t affect intelligence and are different from intellectual disabilities. People with LDs have specific issues with learning but have an average or above-average IQ (intelligence quotient).

I acknowledge that I was including autism as a learning disability, but I see this isn’t the case. Still, however, I hope you would acknowledge that autistic people are not inherently less intelligent than others, and neither are people with depression nor anxiety.

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 mental disorders, which would be a disability). In fact, it’s quite the opposite: the word “disability” exists _precisely_ to distinguish “intelligence” – which is what the university is selecting for – and other characteristics, so in theory intelligence and disability are entirely orthogonal (apart from the exception I mentioned).

Of course, understanding what disability actually is requires considering each learning disability separately, which is something this article unfortunately fails to do. We can do this though:

- Anxiety and depression: I see no reason why this should decrease somebody’s intelligence, so the fact that there are elevated rates of such people at top universities does not seem odd. Since these are treatable conditions, they won’t necessarily affect the ability for a student to become an effective researcher.

- ADHD: This condition is marked by a lack of ability to focus, which is a property unrelated to intelligence. Some very famous mathematicians like Paul Erdős likely had ADHD, demonstrating that it’s not necessarily true this condition makes one a worse researcher.

- Autism: Does not necessarily reduce intelligence. We can look at professional mathematicians and see that a lot of them are autistic.

- Chronic pain, migraines, etc: Unrelated to intelligence. It’s possible this will decrease one’s ability to be a researcher, but if one is able to complete University at all, it’s likely not that severe.

I mean, I could go on, and of course there will be a couple of counterexample. However, it is still the case that generally speaking, “learning disability” and “stupid” are different things, and therefore there is no reason to expect that there would be lower rates of learning disabilities among those who are highly academically skilled.

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?

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 critical thinking is going to suffer most. I still have not met someone who was homeschooled who was remotely thankful for it.

Honestly, support for these policies that benefit, more than anyone else, abusive parents, makes me suspicious of people’s motives.

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 the types have no useful distinguishing characteristics: it is consistent to add the axiom `Nine = Unit` to the type theory. For the same reason, it is consistent to add `ℕ = ℤ` as an axiom.

So a Nine type with a single constructor is indeed isomorphic to Unit but it's not the same type, it carries different syntactic and semantic meaning and the type system preserves that.

It carries different syntax but the semantics are the exact same.

Type theory is usually intensional not extensional so two types with the same number of inhabitants can have wildly different structures

It is true that type theory is usually intensional. It is also true that two types equal in cardinality can be constructed in multiple different ways, but this has nothing to do with intensionality verses extensionality – I wouldn’t even know how to explain why because it is just a category error – and furthermore just because they are constructed differently does not mean the types are actually different (because of the cardinality model).

Cardinality is a set-theoretic notion but most type theories are constructive and syntactic, not purely set-theoretic.

I don’t know what you mean by this. Set theory can be constructive just as well as type theory can, and cardinality is a fully constructive notion. Set theory doesn’t have syntax per se but that’s just because the syntax is part of logic, which set theory is built on.

most type theories don't enforce full parametricity at runtime

What is “most”? As far as I know Lean does, Coq does, and Agda does. So what else is there? Haskell isn’t a dependent type theory, so it’s irrelevant here.

---

Geniune question: Where are you sourcing your information from about type theory? Is it coming from an LLM or similar? Because I have not seen this much confusion and word salad condensed into a single comment before.

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 irrelevant at runtime). So your Nine type doesn’t really make sense, because you may as well just write Unit. In general, there is no amount of introspection into the “internal structure” of a type offered; even though parametricity does not hold in general (unless you postulate anticlassical axioms), all your functions that can run at runtime are required to be parametric.

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 realize you’re talking about 49% – that is, under half, so definitively not “most” – of the US of A’s population?[0]

[0] https://www.nbcnews.com/politics/politics-news/poll-american...

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.

“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 English-speaking viewer. So the question is whether the original was intentionally trying to come across euphemistic, or whether the original was using formal/polite language solely because of its position as being on TV.

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 cardinality than its powerset.

Actually, I can recount the proof here: Suppose there is an injection f: Powerset(A) ↪ A from the powerset of a set A to the set A. Now consider the set S = {x ∈ A | ∃ s ⊆ A, f(s) = x and x ∉ s}, i.e. the subset of A that is both mapped to by f and not included in the set that maps to it. We know that f(S) ∉ S: suppose f(S) ∈ S, then we would have existence of an s ⊆ A such that f(s) = f(S) and f(S) ∉ s; by injectivity, of course s = S and therefore f(S) ∉ S, which contradicts our premise. However, we can now easily prove that there exists an s ⊆ A satisfying f(s) = f(S) and f(S) ∉ s (of course, by setting s = S), thereby showing that f(S) ∈ S, a contradiction.

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 mathematicians for the last century; are you trying to make the point that this part of the curriculum is unnecessary, or that mathematics has not contributed to the wellbeing of society in the last hundred years? Both of these seem like rather difficult positions to defend.

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 seems you have chosen a rather deficient definition of “working with” that does not match with how that phrase is used in the real world.

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 that we can’t know a natural number either! Take 2: you can picture two apples, you can imagine second place, you can visualize its decimal representation in Arabic numerals, you can tell me all its arithmetical properties, you can write down its construction as a set in ZFC set theory… but can you really know the number – not a representation of the number, not its properties, but the number itself? Of course not: mathematical objects are their properties and nothing more. It doesn’t even make sense to consider the idea of a “raw” object.

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 computer scientists unhappy, but this isn’t a project for computer scientists.

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.

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 small number of primitive type formers (e.g. Π, Σ, = and Ω).

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/4076545):

- ℕ ∪ {∞}

- Cardinal arithmetic

- ℤ[x]⁺

Obviously, not all theorems that are true for the natural numbers are true for cardinals, so it seems misleading to say that theorems remain the same. I also believe that the addition of induction increases the consistency strength of the theory, so it’s not “just” a matter of expressing the theorems in a different way.

I would agree more for axioms that don’t affect consistency strength, like foundation or choice (over the rest of the ZF axioms).

Relevant to this is Skolem’s paradox (https://en.wikipedia.org/wiki/Skolem%27s_paradox), which states that any uncountable set can be modelled by a countable set.

In that light, the statement that the reals have greater cardinality than the naturals can be thought of as a statement that _our model of set theory_ happens to contain no injections from the reals to the naturals. Not that they can’t exist in a Platonic sense, or even just in the metatheory.

The Cartesian product of nonempty sets is nonempty. > This is obvious!, you might say — obviously we can just pick one element from each set and be done with it. But the statement that we can pick an element from each set is the axiom of choice.

No? I don’t see how this relates to AC at all. AC is about making an infinite number of choices at once – if you’re just making two choices (or, more generally any finite number of choices), as is needed here to prove that this Cartesian product is nonempty, then that’s completely fine without extra axioms. See for example https://mathoverflow.net/q/32538

E.g. in type theory, one term of type `Nonempty(A) → Nonempty(B) → Nonempty(A × B)` (supposing that `Nonempty` is defined as the [bracket type](https://ncatlab.org/nlab/show/bracket+type)) would just be `λ [a] ↦ λ [b] ↦ [(a, b)]`.

AtomicWaker is much less bad, because it will only spin in the case that another thread has spuriously called `wake` – i.e. called `wake` despite that fact that the future it’s waking is in fact unable to progress.

In the common case, the waker side will operate some logic like:

    set_flag();
    atomic_waker.wake();

    atomic_waker.register(cx.waker());
    if flag_is_set() {
        Poll::Ready(())
    } else {
        Poll::Pending
    }

I can’t immediately think of examples where support for spurious waking is necessary.

Absolutely! The right kind of error type really depends on use-case — I targeted this kind of use case because I see people get it wrong most often, but it’s definitely not a one-size-fits-all solution.