HN user

bitdizzy

276 karma

[ my public key: https://keybase.io/bitdizzy; my proof: https://keybase.io/bitdizzy/sigs/CWf8_sulAck0EfbU3JHdemp3iO1gV6L0pSGaK69XGNQ ]

Posts2
Comments126
View on HN
Renaming Coq 5 years ago

I've been following this discussion closely because I work in adjacent areas and have dipped into Coq and Agda. Now that I see it on hackernews and all sorts of comments speculating on how this is cancel culture and English-centric chauvinism I'm really disappointed. Sometimes you lack the social context to evaluate the merits of a discussion so you default to your image of the most plausible motivation and it says a lot in this case. A popular idea here is the "gellman amnesia effect", yes? Well I'm definitely not going to forget this in the broader context every time a post comes around baiting culture war rhetoric.

Unfortunately some women actually in the Coq community discussing this on Twitter noticed they were getting all of a sudden a lot more engagement with concern trolls around the time this submission gained traction. "intellectual curiosity" indeed. I hope its worth it, this place existing. I think I can find a replacement though so I'm logging off indefinitely.

Almost by definition society is the negotiation of our behavior toward each other because otherwise we would impinge on each others' freedom to act as we please in intolerable ways.

Perhaps you think that is a bad thing and to be honest i wouldn't blame you if you decided to ignore all laws and norms of society and behaved like a feral animal towards others. I just don't think you would get very far before you're put in a cage or gunned down.

What people say are their values and the values revealed by their actions can be different. Moreover one can express certain values in pursuit of goals that are incompatible with those values. This is styled hypocrisy and the bourgeoisie such as Thiel are very used to this.

I am curious as to how?

Special relativity describes a flat lorentzian manifold. The uniform expansion of the universe implies that the curvature of spacetime is slightly negative.

Special relativity is not simply a theory of causality but specifically of the geometry of spacetime. From this theory you can derive predictions about specific phenomena, like causality.

But that doesn't mean other spacetime geometries don't share properties with flat minkowski spacetime. Just not all properties. For example there is no cosmological horizon in minkowksi spacetime but there is for our universe.

Non-measurable sets are precisely the kinds of things Arnold wanted marginalized in mathematical pedagogy, instead of placed front and center. They are necessary auxiliaries to the main theory, that of measures and integration but auxiliary nonetheless.

I disagree that transfinite numbers are detached from physical intuition since most of the ones you or I could write down can be easily visualized with a few ellipses here or there. But i do think Arnold would consider them marginal players. Perhaps he thought set theory was a formalist distraction from the main of mathematics!

The first use of complex numbers was as intermediate quantities in the calculation of the roots of cubic polynomial functions. This use is analogous to using negative numbers in a ledger even though negative amounts of physical things don't make sense.

Edit: I meant physical things like apples fam. This is an important philosophical point we don't appreciate because we are so used to them. De Morgan once wrote:

"It is not our intention to follow the earlier algebraists through their different uses of negative numbers. These creations of algebra retained their existence, in the face of the obvious deficiency of rational explanation which characterized every attempt at their theory."

For Arnold, mathematics is rooted in physical intuition and experimental inquiry. Can you name some math that is completely disconnected from that intuition?

A lorentz boost is just a change of perspective. Let's say you have a bubble that is at rest with respect to your reference frame. Well, someone flying by your solar system has just as valid a reference frame as you and they see the bubble moving with respect to them. The relation between their point of view and yours is described by a lorentz boost. Same physical situation, different perspective.

Now, if special relativity holds in the large then there is no reason why they can't also construct a warp bubble. Relative to you and your bubble that bubble is in motion. Since this is allowed, we can construct a closed timelike curve with two judiciously chosen bubbles.

Which the universe kinda already does, no?

The expansion of the universe does violate special relativity but not in a way that protects warp geometry from creating paradoxes. The kind of violation you would need would distinguish between frames of reference that SR says are equivalent.

And further, doesn't special relativity already only hold in cases with low gravitational potential - so i.e. not in a gravitational field?

Special relativity holds well enough in most situations that the same argument applies even if you accounted for general relativity except near extreme situations like black holes

Warp drives are not permitted by any deviation from special relativity. You need specific contrived geometries of the entire universe that don't match up with what we know about it.

So the thing that paper does is it assumes you can make warp bubbles in any reference frame. The original paper makes one warp bubble and this doesn't lead to anything paradoxical.

But if I can make two warp bubbles in two different frames, I can make a round trip that arrives before it starts.

So you need to violate special relativity in a global way to avoid these issues. You have to have a spacetime where only certain warp geometries are possible.

I apologize for being a bit impatient before, these issues are subtle. The only real way to get it is to bear with the math onesself.

The name tachyonic antitelephone is a bit unfortunate because it need not involve tachyons. All it takes is the ability to send a message outside of your light cone. Along the path actually taken need not be the case, we are reasoning about the endpoints of the communication independent of the means.

In particular it does not matter whether you use a warp drive or not. The violation occurs relative to reference frames outside of the warp bubble where special relativity fully applies. Here, explicitly looks like a worked out example: http://exvacuo.free.fr/div/Sciences/Dossiers/Time/A%20E%20Ev...

You can create instances of FTL travel or communication that don't violate causality. But the ability to perform such FTL tricks implies the possibility of constructing a closed timelike curve so long as you're talking about a localized phenomenon like a warp drive or tachyon where special relativity holds outside of a negligible area.

If you're messing with the global geometry of spacetime then you can make very weird things happen and I would not be surprised if there were such a geometry that allows FTL communication in a limited way that doesnt allow CTCs. But that would not like our universe or a warp drive, a specifically localized situation.

I got a batch of medlars from a farm this last winter! We ate the first few too soon but the rest were amazing, and very late into the winter when we dont really have fruit besides apples. I'd love for these to become mainstream again.

Since ssrn is like social science arxiv let's just throw preprints around. This paper examines the submitted one as well as another.

https://arxiv.org/abs/2010.16084

This paper examines discrimination based on startup founders' gender, race, and age by early-stage investors, using two randomized controlled trials with real venture capitalists. The first experiment invites U.S. investors to evaluate multiple randomly generated startup profiles, which they know to be hypothetical, in order to be matched with real, high-quality startups from collaborating incubators. Investors can also donate money to randomly displayed startup teams to show their anonymous support during the COVID-19 pandemic. The second experiment sends hypothetical pitch emails with randomized startups' information to global venture capitalists and compares their email responses by utilizing a new email technology that tracks investors' detailed information acquisition behaviors. I find three main results: (i) Investors are biased towards female, Asian, and older founders in "lower contact interest" situations; while biased against female, Asian, and older founders in "higher contact interest" situations. (ii) These two experiments identify multiple coexisting sources of bias. Specifically, statistical discrimination is an important reason for "anti-minority" investors' contact and investment decisions, which was proved by a newly developed consistent decision-based heterogeneous effect estimator. (iii) There was a temporary, stronger bias against Asian founders during the COVID-19 outbreak, which started to fade in April 2020.

He wasn't just a white supremacist, he developed the framework he did specifically because he wanted to elevate certain forms of music as superior and "White".

Using Music theory is like using English as the tech lingua franca instead of Latin or Esperanto, it's not about imperialism, it's just too troublesome to learn and change and does the job pretty well anyway. The idea that ideas carry over all of the context of their creation is simply insane.

English is a natural language and all technical concepts are equally well expressed in most natural languages perhaps with the need to enrich the vocabulary.

A specific framework for analyzing music which emphasizes certain specific structures and discards considerations that other musical traditions hold as important creates systematic biases in the understanding of music.

A better metaphor would be perhaps be expressing algorithmic ideas in a language where only "for" loops were deemed important and everything else a derivative concept.

The fact that you think this bias towards specific forms of European music doesnt have consequences doesnt make the idea insane. I think the fact that you have to resort to that kind of labeling speaks to a fragility in your worldview.

I dont know which video you watched but it's basically true that what most people call Music Theory focuses much of its attention on a narrow period of music on a narrow continent within narrow analytical frameworks (Schenkerian, for example) and comes associated with a lot of normative baggage about what is valuable and interesting in music and what is not which is biased towards specific musical traditions which, surprise, are white.

Schenker himself admitted to white supremacist values in the development of his ideas. Of course it was en vogue at the time.

The music under study isn't white supremacist itself of course, nor is the structural analysis. Whiteness is usually imputed post hoc by less talented hangers-on.

It's not an axiom. It's a fundamental disagreement about how society should be and an understanding of what the world would be like if nazis have the power to change it to suit their vision.

It's people like you that inspire me to counteract this trend with full force.

What does that look like? What actual effects on the world do you try to make or support others making because I am opposed to fascism?

It is entirely and issue of the means of communication being concentrated into the hands of a few powerful organizations, like its been since the radio was captured by capitalist regulation.

Who the fuck decides? Everyone decides norms in the small bubble around them. When people organize their influence grows too. Some people have too much power. Some people should never have power, like nazis.

A lot of the arguments in this thread you will notice are about whether deplatforming makes nazis less nazis. Well, that's not the point. The point is to make sure they aren't accepted, that they can't use the public square to recruit and gain power.

Some would argue that this is ineffective, but they are now stuck in the bind of thinking that access to places of public discourse is both an important right and also practically unimportant.

Maybe they're too young to remember the holocaust deniers on use usenet or how ineffectual stormfront was before 4chan and before mass social media. People who are hungry for power will try to gain it in the easiest ways possible.

If you think them having power would suck, then you want to make it harder for them.

I simultaneously think facebook and twitter and CBS and fox news etc. have too much control over public discourse and also don't want white supremacists to be able to freely use that power to bring back hell on earth. That includes the new york times giving the likes of Richard Spencer space on their page, Tucker Carlson crying about how much white people are under attack and facebook letting white supremacists run recruiting groups thousands in size.

The weirdness of quantum mechanics with respect to bases is very counterintuitive but makes perfect sense internal to the logic of the quantum world. It is a sort of relativity where there can be incompatible viewpoints.

Namely, a hermitian operator is some view of the world, its eigenbasis tells you what you can see from that viewpoint. Two hermitian operators can be incompatible in that they can't be simultaneously diagnolized.

Entanglement is another weirdness that makes perfect sense internally. The tensor product of projective hilbert spaces is not the same as the cartesian product. The segre embedding captures this. Theres more to the geometry of quantum phenomena than naively expected.

The outcome of measurements collapsing to the eigenbasis of a hermitian operator has a beautiful an elegant geometric interpretation. It makes perfect sense really, just not classical sense. Decoherence explains why we see collapse to this set very well.

What is utterly baffling and puzzling is that we only ever see one particular outcome. Decoherence cannot explain that and nothing in quantum mechanics explains that.

Do you think the distinction between government interdiction and private is immaterial? I think I regard the distinction between business and government a lot less than most but still understand that there are significant differences between the two and some people think those differences are extremely important.

But what is meant by tribalism?