Comments URL: https://news.ycombinator.com/item?id=7327950

Points: 1

# Comments: 1

It's not quite a blog post, but it's as close as one might have come in 1908.

I also like a whole host of articles from Matt Might's blog. I think my favorites are

12 resolutions for grad students

http://matt.might.net/articles/grad-student-resolutions/

and Responding to peer review

http://matt.might.net/articles/peer-review-rebuttals/

One last essay that I have enjoyed, also too old to be a blog post, is W.M. Turski's "I was a computer". It's here on Elsevier but fortunately it looks to be open access.

https://www.sciencedirect.com/science/article/pii/0167642395...

[0] http://siek.blogspot.com/2012/10/is-typescript-gradually-typ...

[1] https://typescript.codeplex.com/discussions/428572

If you're saying that perfect pitch and relative pitch are different things in that it isn't as if perfect pitch is better than relative pitch, then yeah, I absolutely agree. The hacks that I mentioned involve perfect pitch specifically, but transcription ability like you mention is probably tied most to one's sense of relative pitch, even if one has perfect pitch.

My brother and I are both musicians with perfect pitch, and we've found it useful in a variety of circumstances. To name a couple, it really helps if you're jamming and want to pick up a progression quickly, or if you're DJing and want to key match. I will concede that Traktor recently got key detection, which is nice, but especially when playing live I find that key segues will pop into my head without having to search for the next song in the right key.

Even the best relative pitch cannot help you exactly memorize a melody -- if you are unable to remember what note it actually starts on, you haven't remembered it fully.

I would be interested in similar pieces from 50 years ago, looking back on 1914's view of 1964. So much has changed since then, though, and it seems like more has changed since 1964 than changed from 1914 to 1964. In particular, the 60s happened, but even after that, the Internet seems to have effected a fairly massive and seemingly permanent cultural shift. It might be too early to tell, but even the fact that someone posted this commentary, we all read it instantly, and then now we're discussing it here only hours later seems worlds away from the climate of 1964.

I wonder if someone at MSR would be interested in taking up the cause and publishing with Joe. It does seem like this work might contain the makings of a great PLDI paper.

I've been playing the Hearthstone beta with a few friends for a couple months now and it is absurdly fun. Also played a bunch of StarCraft II and Diablo III as usual.

Skyrim and Fallout: New Vegas have held up well. Papers, Please was just fantastic. I had fun playing CounterStrike: GO with friends.

I played SimCity and liked it, though in the midst of the fallout and server issues, I found Tropico 4 and Anno 2070 to be fantastic alternatives.

On Black Friday I picked up a PS3 and have finally been getting into The Last of Us, which is stunning, and Red Dead Redemption, which I think will take longer to get into.

I want to lastly point out that we've had a lot of fun doing LANs with some classics that we've been playing for years now: CS: Source, Rise of Nations, Age of Empires II.

[0] http://ssrg.nicta.com.au/projects/seL4/

Comments URL: https://news.ycombinator.com/item?id=6936210

Points: 5

# Comments: 4

One particular observation that the article makes that I want to flesh out a bit is the following: Facebook has grown and grown in terms of the size of the application itself, and it is clear that they have pushed very heavily for the 'platform' model. It seems like this is getting replaced by a series of more specialized, more mobile-centric social applications, like Snapchat and Tumblr. Of course FB owns Instagram so they have that going for them, but this does seem to hint at a bit of a growing trend in social networking.

At this point we are mostly debating what "can use" means -- it's probably enough to say that unless you reframe your thinking, perhaps radically, probably it will be hard for you to be able to use HoTT to get work done. It is possible to do classical mathematics within HoTT, in the normal way, but it would not be very fun.

What is meant by "even if it wasn't, it would still work" goes back to something he said earlier: type theory embeds an infinite hierarchy of axioms of choice and laws of excluded middles. If you want to do propositional-like reasoning in homotopy type theory, you can assume AC or LEM for homotopy (-1)-types, corresponding to propositional logic.

In type theory you are encouraged to drop the law of the excluded middle and the axiom of choice, because of the fact that doing so gives you potentially more expressive ways of doing things as we have said, but you have gotten the impression that you have to, which you don't.

Also, the claim in this thread was that the results from classical mathematics are provable using homotopy type theory, not that they are provable in the same way (though that holds as well, as I've said above; it's just that the mathematics might not look as clean as if you did it in a more idiomatic way). This kind of a value proposition is not exactly new: category theory loses certain axioms over set theory and mathematicians adapted to the point that category theory is now the language of modern algebra.

I want to point out that I suggested that you read the introduction to the book because it provides these same answers to the questions you are wondering about. I still suggest you do so, as it goes into more detail on what we have said here in a way that I am not able to quite as well.

The emphasis that you are placing on the fact that type theory happens to be a constructive logic is perhaps causing you to miss the point. Homotopy type theory is not about advocating constructivism. The "big idea" is that HoTT is a foundation that computers can already reason about easily, based on the work that has already been invested into developing sufficiently powerful dependently typed languages (Coq, Agda). Because it is possible to formulate set theory, category theory, and even real numbers (all discussed in part 2 of the book) within the framework of homotopy type theory, it should be possible to extend these formulations to encompass more and more results from the rest of the mathematics. Because HoTT has already been shown to be implementable (in the form of a library for Coq), this means that any math that is done informally under homotopy type theory can be carried directly into a formal, machine-checkable series of theorems and proofs, in the form of a Coq development.

To expect this material to be readable and useful to every average Joe right away is asking far too much of any new idea in mathematics. This is cutting edge research, and there is still too much even the people closest to this material don't understand yet. As another comment on yours alluded to, at one time your equivalent in the 1700s would have written off calculus as indecipherable and judged it not likely to succeed as a result.

1. Despite your claim that you are not versed in type theory, chapter 1 provides what I find, as a 21 year old graduate student in programming languages with a relatively standard undergraduate background in mathematics and then some, to be a clear and helpful explanation of Martin-Löf type theory, and a good exposition of background needed for chapter 2. Did you read it?

2. This book makes extremely clear that the "homotopy theory" that is developed towards the exposition of homotopy type theory is merely synthetic, which is to say that it considers homotopies as first class objects, rather than deriving them from their traditional topological underpinnings in a more analytic way. It might be useful to have a little understanding of point-set topology with maybe a little inkling of what's going on in algebraic topology to figure this out, but certainly it doesn't seem absolutely necessary, since the book's notion of homotopy is built from first principles. Are there specific points in chapter 2 that you find confusing?

3. It appears you have a doctorate in CS, specifically to do with interactive theorem proving. Almost every proof assistant I have come across either uses dependent types or higher-order logic, and it seems like in order to have earned a PhD in interactive theorem proving you might have had to have become familiar with at least one of these formalisms. Given that you should be comfortable in one of these domains, it doesn't seem like the material in the book is a huge leap. Could you speak a little bit more to what you worked on grad school?

I don't mean to come across as harsh, but your claim that this book excludes 99% of its target population seems false; at the very least I do not consider myself in the top 1% of people who might hope to consume this book.