Alice Coltrane rocks.
215 karma · joined April 14, 2014
Interesting idea about the reveal! I’ll consider adding that (or some cheap version of placing the image in the success modal at least).
Perhaps clone is a poor word here and inspiration would be more accurate.
The main objection is that most proof-assistants use a different logical foundation than modern mathematics. Modern mathematics is built on ZFC[0] whereas most proof assistants, such as Coq, Isabelle, Agda, etc use different logical foundations, such as the Calculus of Constructions[1].
Many important results in modern mathematics are not easily stated or proven in systems such as CoC[1]. For example, Brouwer's _Fixed Point Theorem_[2], a pretty bog standard result in Topology that is useful to proof many things in Functional Analysis, has a clear statement in ZFC, but does not, to my knowledge, have an equivalent in CoC (and if it does it will be stated radically different).
[0]: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... [1]: https://en.wikipedia.org/wiki/Calculus_of_constructions [2]: https://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem
If you are hiring, please reach out to people from SoundCloud. The decisions of who to let go were not based on performance. A lot of amazing people, both attitude and technically.
- getting dark around 4/5pm - extremely dry and cold - winter starts in October, lasts until late April - massive urban sprawl so the city core is dead during the winter, and therefore the city feels lifeless.
That's particularly bleak and definitely biased, but it's not far from the truth.
On the other hand, as someone who grew up in edmonton, I don't ever want to live there again. It's a tough city to live in, though it has its beauty when you look hard enough.
We are looking for an impact-driven Senior Data Scientist to solve exciting problems in recommendations, search, and personalization using Machine Learning. As a Data Scientist at SoundCloud you will work closely with other data scientists and engineers to find opportunities and build, tune, instrument, and evaluate machine learning models.
Some projects you might work on include:
* a personalized playlist recommendation model to empower curation at SoundCloud
* offline evaluation to improve the search experience of our users
* prototyping deep neural networks and demonstrate their benefits in powering recommendations for our users
* iterating on our Spark-based locality sensitive hashing implementations to improve recall.
I'm an engineer on SoundCloud's Recommendations team. We are looking for scala engineers to help users find lit tracks on the world's largest audio platform. You'll work alongside data scientists and engineers in a stack based on Spark, Scala, Finagle, and Cassandra.
SoundCloud is a wonderful place to work and Berlin is an amazing city to live in. I relocated from Canada and haven't looked back.
Empfehlungen sind die Zukunft!
job link: https://soundcloud.com/jobs/2016-08-04-backend-engineer-disc... blog: https://developers.soundcloud.com/blog/tracks
PS - ping me on LinkedIn (https://www.linkedin.com/in/aaronmblevin) so I can refer you!
https://soundcloud.com/jobs/2016-02-19-search-engineer-berli...
It's actually more of a critique of current leftist ideas (from a Left perspective) than anything.
quote:
Getting less work seems unlikely to come about without the fight for solidarity, the chief intellectual achievement of the workers’ movement, and one that none of the accelerationists see fit to mention as an ideal worth preserving or even renovating. This is despite the fact that automation—or, more broadly, the increasing precariousness of labor through technologically assisted means—has always been dialectically connected with it. What tech enthusiasts call“disruption” is in fact almost always directed at forms of organization that preserve a modicum of workers’ control over knowledge and the products of labor. Because London taxicabs are controlled by people who have built up impressive maps of one of the world’s most complex cities in their brains, they ought to be replaced by self-driving cars operating on Google Maps. Because high school teachers have professional systems of accreditation and training and have unions to protect these, they must be replaced by lower-paid short-term Ivy-League graduates and cyber charters.
Automation isn’t a neutral, inevitable part of capitalism. It comes about through the desire to break formal and informal systems of workers’ control—including unions—and replace them with managerially controlled and minutely surveilled systems of piecework. An entire political and legal infrastructure has been built up to make these so-called tendencies seem like the natural progression of capitalism, rather than the effects of fights—sometimes simple, sometimes violent—to deprive people of whatever sense of control they have over their work. The only reason such work has ever not been totally shitty is that some attempt to preserve such control was made. This — not some implausible notion of a fully automated postwork future—still remains the surest of utopian impulses, the one most likely to deliver the things we want.
Though the times are bad, the accelerationists presume that the state of the left will get better simply because it can, in principle, get better. An imaginative (if implausible) account of the future, accelerationism is a weak account of how anyone might be persuaded to get there. We recall Lenin’s comment about how communism would be “Soviet power plus the electrification of the whole country.” The accelerationists seem to be telling us: forget about the Soviets, the electricity will do that work for us! But politics can’t get done by machines.
Marx's "theory" was a method of analyzing history by focusing on class conflict as the main driver for history. By applying that analysis to capitalism, he predicted that the proletariat would inevitably come into conflict with the bourgeoisie. Das Kapital was a deep dive into how and why this conflict comes about (both economically and philosophically).
As for what happened next, those are "implementation details" which Marx didn't write too much about. We've seen a few implementations (Bolshevism, Stalinism, Cuba, Maoism) and a few modern contradictions (current China, North Korea, etc.) and most have been flawed.
However, not every implementation of capitalism has been successful, either. There are plenty of fascist and repressive states that are capitalist. Nazi Germany and Italy during WWII, Argentina during Pinochet, hell, you might even say ISIS is capitalist.
So, I'd argue that many implementations of communism have failed in the same way that several implementations of capitalism have failed, but there is a large space for experimentation as there has been with capitalism. For example, democratically planned economies with analytical input is a space that hasn't been explored too well beyond very tiny experiments in sectors within Latin America.
Semantics! :)
In many cases you are not guaranteed via the type system that one individual's implementation of the Observer pattern (for example) is not full of bugs, contains side effects, or closely adheres to the pattern's spec.
I believe Gabriel is hinting at the theoretical underpinnings of what it means to be composable, as opposed to just talking about how things can be mashed together (via pattern or interfaces or contracts or testing or whatever).