HN user

zepolud

928 karma
Posts9
Comments58
View on HN

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.

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".

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.

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.

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.

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.

"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.

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.

'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

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.