HN user

amvalo

345 karma
Posts0
Comments121
View on HN
No posts found.

From what I understand, Parler was bankrolled and designed to do exactly what it was ultimately shutdown for. That is, be a concentrated anger-machine-echo-chamber. I'm not angry at the public corporations that have dropped Parler. I'm angry at the people that created Parler in the first place.

Where did you get this understanding? Seriously. My understanding was that the founders were mostly anti-trump libertarians.

how much of this nuance is achieved by having discussions about issues which have real life-or-death impacts on people but without having any of those people inconveniently present?

Uh, not much? This comment seems to be assuming some weird things about what the blog typically focuses on. Actually, he writes about trans issues a bit, got some flack for defending Blanchard, and a large fraction of the readership is trans.

The biggest pain point with the theory was its handling of equality, which HoTT fixes.

Ergonomically.. well it's hard to describe TBH, the easiest way to see is to just download one of these systems and try using them. You try to prove a theorem and everything just ends up taking way longer than you'd expect. Mostly because you can't gloss over small details the way mathematicians will do informally. Every small turn of phrase like "for large enough N" or "without loss of generality" can become dozens of extra lines of code.

The answer is simple: these systems aren't mature enough to formalize the modern fashionable math. They need better ergonomics and perhaps better underlying theory before we attempt that.