bbeonx

I don't know, I might push back here. While fake news can certainly be interpreted as news that is false, that is not how it is usually used. There is definitely an insinuation, and while the vanilla reading of the definitions of "fake" and "news" don't contain this insinuation, it exists none the less.

That being said, as a writer I might not be able to resist pointing out the irony that the paper on fake news was fake news :). I really can't fault the author.

Do what?

Look into the Coq language, it is under active development and there is a lot of work going into it. Voevodsky was working in Coq, if I recall.

As to how hard it is to learn, you will have to learn a pretty decent amount. It all depends on your background. If you know what the Curry Howard correspondence is, you are in relatively good shape. If you've never heard of lambda calculus or first order logic, you may have some more work cut out for you.

Here is a nice article I read last night on explaining the move from set theory to type theory. It gets a bit technical but you might be able to get something from it.

https://golem.ph.utexas.edu/category/2013/01/from_set_theory...

Oh cool, this is from Allen Hatcher. I've worked through some of his algebraic topology and it was very well written. I'm excited to look through this

rolls up sleeves alright, folks, let's get to it

Ahhhh, but then they will ask how to print things and you'll have to explain monads :)

Biggus Uptickus

I don't know why people keep posting about this. It really doesn't matter

Just a heads up, there are two types of semigroups out there, and I think that automata theory uses the weird (i.e., non-algebraic) kind, so don't be too disappointed if this doesn't hook in with other standard maths. I have only seen this second usage of semigroups in automata theory, and only heard it used by an automata theorist. A quick Google search didn't turn up this other usage, so it seems to be very domain-specific lingo.

On the other hand, you can look into algebraic automata theory (a subject I know nothing about) and play with monoids (the kleene closure of an alphabet with the concatenation operation is the free monoids over that alphabet).

I feel like these are both excellent points.

Out of curiosity, what wasn't clear aside from openness?

BTW, for those interested, openness is the property assigned to a set of points not containing its boundary. For instance, an open interval (a,b) doesn't contain boundary points a or b. An open unit square is a 1x1 square without it's edges included

Yeah, it assumes basic algebraic topology (which is not a mild assumption). He states at the top that he is assuming familiarity with homology groups, and chain complexes are used to define homology groups.

So you're saying Python devs are all libertarians? :D

<braindump>

I agree that coding/development is an art, but I also am hard pressed to find anything that, when done well, isn't an art.

The difference is that music doesn't have any really notion of correctness or efficiency; sure, there are ideas such as "no parallel fifths" and "tritones must resolve to M3 or m6", but this isn't an issue of correctness, but rather stylistic guidelines. Schoenberg's compositions weren't incorrect in any universal sense.

Programs, on the other hand, can be incorrect or inefficient. This is because most programs have a concrete function that they produce.

Dynamic types are great for exploring your solution space. I can quickly whip together a prototype, try out different solutions, etc. I don't need to design my entire program ahead of time, and this is nice. However this does not prevent me from reasoning formally about my program. Once I've muddled around a bit and built up some scaffolding, it very well may behoove me to try to shore up my design, spend some time reasoning and designing a formal algorithm/specification/etc, etc.

And for the record, as a musician I definitely think formally about my compositions/pieces I'm playing. Granted, being a guitarist this usually doesn't involve me writing out my pieces with sheet music, but there is still a blend of intuition/exploration and brute computation.

As an example, I often times have two disparate parts that I need to connect together, maybe by modulating, maybe by changing registers, or maybe by altering my time signature. At that point I put the guitar aside for a moment and think about my formal requirements, and then try to find some 'convincing' way to get from point A to point B. Maybe I have some constraints (I have two measures, I need to start in this position and end in that position, this finger needs to pedal this note, etc). This quickly becomes a math problem where only a small set of viable solutions exist. After 'doing the math' I am left to evaluate my solutions aesthetic quality which, I suppose, is where most people think of the 'artistic' bit comes into play. But really, I'd say artistry abounds throughout the process.

And to be clear, I'm not thinking about this stuff as doing math as I'm doing it--I have my own system for thinking about this stuff that doesn't look like math.

Anyway, all of this is to say that formalism can be used even in music with very real benefits.

</brain-dump>

Nice, I'm posting the Legendre's constantst comment in this thread

My guess is because OP has been burned by the "LEARN THIS NEW THING, IT'S REALLY COOL AND POWERFUL AND ALL OF THE COOL KIDS ARE DOING IT (and oh by the way many of the simple things you do all the time are incredibly inconvenient...)" narrative one too many times.

Adopting something purely on it's merits is a bad idea, but nobody ever writes the book about a language/paradigm's downsides. I'm pretty sure that was the joke, but I might be off.

Actually, I'm curious why people don't like white space sensitive languages. I get the tab v space thing, and there are certainly a couple of other down sides, but none of these seem like deal breakers to me. Given that python was the second language I learned, it's possible that I drank the coolaid early and I'm blind to some things that are truly egregious.

So the question is: why do folks completely avoid a language for a single relatively bland syntactic feature? Is there some cost I'm not aware of, or is it just stylistic/aesthetic?

Which is, of course, just a fancy way of writing (-7:30) to 03:00

Yeah, this made sense to me. It took me a minute but I got there. The general strategy is "binary search" which doesn't make for a good article :p. Also, the details of actually implementing the strategy are difficult so an example was useful for me (not that I will ever play this game, but hypothetically...)

Right, I need two keylocks 7 feet apart that need to be turned simultaneously after a security code has been punched in.

I second On Writing Well. Great book, and fun to read.

It's funny, editing has always been my favorite part of writing. It's when all of my favorite bits typically get written.

I agree, I like the name.

IMO, even if gerrymandering doesn't have a huge effect on seating in Congress (perhaps it has more effect on state level politics? I didn't read the other commenter's link so I won't make any claims) it makes a lot of districts non-competitive. The effects of this are hard to quantify and so we don't hear as much about it, but I argue that they are at least as profound as the numerical differences in congress on our national dialogue.

Ahh, thank you. I was very confused

Semantics. What I should have said is "when the valuation of a wide percentage of peoples earnings and assets who belong to an industry suddenly decreases from unforeseen outside forces caused by rapid technological advances..."

Or how about "when about 18% of taxi drivers nest egg devaluates and their retirement evaporates..."

To claim there is no difference between a restaurant failing and all independent taxi cab drivers in NYC simultaneously taking a giant hit that they did not see coming based on an (admittedly bad) policy of protectionism, is intentionally missing the point and I would say is intellectually dishonest.

Is a bailout the best way to fix this? I have no idea, seems like a relatively low cost way to fix what the city did but these things are complicated. I'm open to that discussion.

Are failure rates of the restaurant industry totally incomparable to this singular situation? Most definitely, and any argument based on this is flawed IMO.

Yeah man, I read that. I stand by my claim.

Oh cool. Yeah, I looked around from "Music Composition Constraint Solving/SMT/Z3" stuff and didn't find anything which was surprising. I'll take a look at Rosette too, I've heard of it a couple times but never dug in

I am writing a Z3 music composer right now actually. Just as a toy project but the idea is solid: you have a passage that you need to harmonize? Here are three different versions that conform to the rules of fuxian counterpoint, etc

Yeah, I've been using z3 for a couple of projects and it is an absolute pleasure.

One of my projects involves I'm.entiong part of the JVMs execution in Z3 constraints and we have been able to prove stuff about program equivalence this way which is exciting.

Once the problems get big enough we will need to find clever ways of shaping Z3s search path, maybe by writing a theory, but for now it works for anything we have thrown at it.

Different strokes for different folks, man. I get off on quantification. I hyper focus and I cannot do anything passive.

Dieting? That's passive: it involves not doing something. All I can think about is the fact that I shouldn't be eating, which makes me think about eating, which makes me eat.

Obsessively counting calories? It makes me do something active: strive for a minimal caloric intake for the day (I say minimal but minimal for me is healthy for anyone else).

I need to do the same thing with reading papers. Reading a paper is a passive activity while writing a paper review is active. I try to find at least one major flaw with each paper I read so that I have something active to keep my attention, a goal.

Saying "behavior xyz is silly" is unfair and not super constructive. Each of us has a single data point of human experience. Generalizing from that is kind of silly if you think about it.

If I could curtail my bathroom activity healthily, and if that would lead to a better and happier life, then dammit I'd track that shit in a heartbeat. Ditto for breathing. And unless you are having an unhealthy amount of sex there is nothing to gain from tracking it (except for ego/lack thereof).

The examples you list above all have something in common: there is no benefit to tracking them. For calories, there is an actual benefit.

Correction: Most taxi medallions are not owned by drivers. There are certainly drivers who own their own medallions (18% as of 2012). This is a non-trivial sector