zepolud

> If you're under enough surveillance that your adversary will follow you on holiday and track all your supermarket purchases, you have bigger problems.

Problem with modern surveillance is not that somebody is actively tracking you, it's the ability to retroactively track you back with perfect accuracy soon as you become become an inconvenience.

Thankfully, Deep Throat wasn't aware of that.

I'm not comparing anything, merely reacting against any attempts to trivialize the very real need for a platform for anonymous dissent.

From the lives of the people involved to the stability of the democratic institutions themselves, those are very real and very high stakes. It would be extremely disingenuous and insulting to pretend that the intent of the article was to anonymously tweet "trump is a poop".

Remember the thousands of people arrested for "insulting officials" on social media in Turkey?

[1] http://www.businessinsider.com/ap-turkey-arrests-1656-social...

Probably, but doing it correctly would require a whole different type of opsec expertise that should not realistically be expected from someone who is getting their security tips from The Intercept.

This addresses shop cameras, not street-level government surveillance that would be accessible for 10+ years and is trivially addressable by the time and location of the transaction.

It would be very irresponsible to recommend buying a burner phone to people trying to stay anonymous. At the very least, it would give away your location even if you somehow manage to remain unrecorded by street CCTVs in the vicinity of the shop at the time of purchase. Assuming it is even possible to buy one without providing full personal details, as is required by law in most of the EU.

Twitter now not only gives platform to powerful demagogues, it is also actively stifling dissent by effectively disallowing anonymity.

What about the laws of thermodynamics, pretty oppressive if you ask me. Better oppose that too.

> I hate admitting it but democracy works pretty well in Turkey.

Majoritarianism should not be confused with democracy.

Take a minute and reflect on the fact that you're arguing Turing had nothing to do with mathematical logic.

His doctoral advisor was Church, his work based on Gödel, his thesis named Systems of Logic Based on Ordinals.

Comments like these show the perils of treating mathematics like a cookbook. It's a very limiting mindset.

Sadly, Turing wasn't aware of this at the time -- think of the real world impact he could have had.

"They say 'there are no atheists in foxholes.' Perhaps, then, there are also no libertarians in crises." [1]

[1] https://www.hks.harvard.edu/fs/jfrankel/CatoRespCrisesJun07+...

Funny how things turned out. I still remember this post[1], it was profoundly disappointing to see Guido's way of thinking. Much of the damage was reversed but it still left an indelible impression that there's a lack of vision for what's going to be important if the language is to stay relevant in the future.

[1] http://www.artima.com/weblogs/viewpost.jsp?thread=98196

It should also be added that most of this work is being done publicly and is open to new contributors. You can check Voevodsky's github page[1], and most of the other HoTT collaborators are active members as well. The HoTT book itself is also being collaboratively written there.

[1] https://github.com/vladimirias

Next keynote by Carmack might be on accidentally solving the Fermi paradox.

Apart from the usual Manifest Destiny IN SPACE! crap, recently I've been a bit shocked to realize that there might actually be a point in trying to go to remote and harsh places.

The Antarctic being a barren wasteland makes it an attractive breeding ground for penguins precisely because it's so inhospitable to anything alive, penguins included. As long as penguins suck less at living in a barren wasteland than their predators it's a net benefit for them to be there, despite the hardships of the environment.

If we assume there is a group of humans that feel existentially threatened by other humans so much that odds of surviving in an irradiated subterranean Mars colony beat the odds of being exterminated here on Earth, it would be a perfectly rational choice for them to try and move somewhere out of reach.

There are lots of potential scenarios why such groups might come into existence, and not all of them involve outright genocide. For example, a group could form just as a result of concerned citizens wanting to go to some place very, very remote once kids start playing Pokemon with their newfangled RNA synthesizers.

It's not even that; it's suborbital.

Please read the context of the first post--I'm referring to the engineers behind the specifically mentioned Buran program, an autonomous spaceplane that launched, flew and landed with no crew.

If the Soviets deemed it too risky for human pilots and managed to automate it 25 years ago maybe that should put it into perspective just how risky and reckless what Virgin are doing is.

The failure modes of rocket engines could be explosions but nobody says you can't have multiple redundant engines on a single rocket. In fact, in 2012 Falcon 9 demonstrated exactly that: one of their 9 Merlin engines blew up but the rest redistributed the load and the rocket successfully delivered the payload to the ISS[1].

[1] http://blogs.discovermagazine.com/badastronomy/2012/10/08/sp...

"These people" that designed the spaceplane didn't put their lives on the line, they put the lives of the pilots on the line. And I would trust the judgment of the engineers at Boeing, Sierra Nevada, SpaceX, Lockheed-Martin and the entire Soviet space program over theirs.

It is demonstrably avoidable, there is zero need to risk human lives when doing testing these days. This is why Sierra Nevada's Dream Chaser has the capability to land autonomously and is precisely why when it had an accident in 2013[1] nobody was hurt.

[1]http://spaceflightnow.com/news/n1310/26dreamchaser/

Test pilots? In the 21st century?

I find it absolutely reckless and inexcusable to require live humans riding on a prototype rocket when you have all the processing power needed to automate/remote manage the vehicle literally in your pocket.

EDIT: To those downvoting, you should really check that all current spaceplanes have the capability to fly and land autonomously--Boeing X-37, Dream Chaser, even Buran was fully autonomous and that was 25 years ago. There is simply no excuse for Virgin for being sloppy.

You should check Olinuxino Lime[1] if you're looking for SATA connectivity. It costs 30 EUR and is open source hardware.

[1] https://www.olimex.com/Products/OLinuXino/A10/A10-OLinuXino-...

>'Safe' programming languages will improve security, presumably at the cost of usability through decreased performance. A bit like how a Ferrari is faster than a Volvo, but not as safe.

This is fundamentally untrue. Safeness of the kind described in the article does not come at the cost of performance -- all type checks, invariant conditions and general formal proofs of correctness are determined at compile time. The produced code is to be indistinguishable from a correctly written, efficient C program. You are allowed to play as much as you like with direct memory accesses and use all the dirty tricks you like as longs as you can prove that the resulting program is formally correct.

What could be argued is that price you pay for all this is the difficulty of writing such programs. But definitely not their performance.

To take it one step further, it might be a good idea to specify the whole thing in Coq, prove correctness and derive the C code from there. Coq is a theorem prover based on the Martin-Löf type theory like the ATS mentioned in the article. Xavier Leroy (the man behind OCaml) managed to write a whole verified C compiler in Coq[1] so while it's slower than writing C directly it should still be feasible for projects of such critical importance.

On a related note, mathematicians are also finding it increasingly difficult to trust unverified proofs. Papers by Vladimir Voevodsky, a Fields medalist and one of the most prominent in the field, were also discovered to contain errors more than ten years after publication, having been cited hundreds of times and nobody noticing the errors in the proofs. This was one of the principal motivations for him to initiate the project for homotopy type theory, which also has roots in Martin-Löf type theory and is also being developed formally in Coq.

[1]http://compcert.inria.fr/diagram.png

> [...] but RSA said in a statement: "RSA always acts in the best interest of its customers [...]

True, you just have to keep in mind that their customer is the NSA.

Created in the same era as Google Code Search and likely to meet the same fate.

He mentions those in relation to his own pet theories but in no way does he address GP's argument.

What his theorem boils down to is:

1. Let A be a formal system capable of describing the natural numbers. 2. Assume A is inconsistent. It follows that there exists such Φ that A ⊢ Φ and A ⊢ ¬Φ 3. ????? 4. A is consistent!

At step 3. he appears to conflate A⊢Φ ∧ A⊢¬Φ with Φ∧¬Φ and use it to refute the assumption in 2. But Φ∧¬Φ is not generally true outside the context of A and therefore the refutation does not follow.

It's safe to assume that most of us accepted that the mass surveillance programs existed. This doesn't diminish the importance of what Snowden did.

It was more of an emperor-has-no-clothes moment than some unexpected, shocking revelation. It forced a lot of people to stop avoiding the problem and to actually start talking about it openly.

It's a lot less poetic if you consider that it wasn't "trust" that brought our placentas into being but a mutated retrovirus.

More power to this guy if he helps people feel better about themselves and the world but he should refrain from entering public debates about "genetic engineering and economics" while presenting himself as somebody enlightened, knowledgeable or even adequately informed.

It is unfair to judge him solely from this article without having read his books but what can be gathered from it and a cursory search suggests that his interest in modern science consists exclusively of surfing the current zeitgeist without actually being interested in science, or even the philosophy of science.

If he indeed is "at the forefront of European intellectual life" it would be a pretty sad testament to the dismal state of contemporary philosophy.