gdp

I would argue that those who would argue that have probably not spent a lot of time doing any real-world formal verification.

People seem to like arguing about its utility in the abstract without ever doing it.

http://adam.chlipala.net/papers/CtpcPLDI07/

(there are subsequent papers too, but that's probably a good place to start).

If you understand a little bit about how something like Isabelle is constructed, only a small number of axioms are "hand coded", and then the rest is built from those. You can always build an external proof checking tool that checks that the proof you've constructed is correct. And if you're not confident in that, you can build another one.

There was some discussion on the original post to HN about this announcement. In particular, look at this:

http://ertos.nicta.com.au/research/l4.verified/proof.pml

Which talks about the limits of provability.

In short, a "proof" that contains errors isn't really a proof of anything. And you build your proof inside an automated theorem prover so that it can be mechanically checked for internal inconsistency (i.e. contradictions), or for a completely inability to be false (i.e. tautologies).

The safety properties might be things like who can write to what memory, and when it is acceptable for bits of the kernel to do certain things. Lock freedom in scheduling is probably also a big thing. I haven't looked at any of this very closely, but I'm just guessing based on the sorts of properties I would try to prove initially.

So it might take 200,000 years to verify Windows, but considerably less to verify an equivalent amount of non-operating system Haskell code, for example.

Hounding people for recommendations will either lead to refusal (which will inspire you to write a blog post about people who don't like you), or people will write you a mildly insincere recommendation to avoid causing offence. At that point, you should be grateful that your acquaintance has considerably more social graces than you do.

> The purpose is to review various people that didn't like me and explore why.

I guess my problem with the article was that the tone implied that most of these people weren't justified in not liking you, or that it was some natural effect of a bad situation, rather than something caused by your own actions.

I think it's just important to pay attention.

Through the description of the actions of each of the people with whom he disagrees, I immediately found myself sympathising with the "other side". I mean, there are the usual dailywtf-style "this guy is really dumb/awful to work with/whatever" stories, and we all get a bit of a laugh out of them, but this just comes across as a situation where the author is unable to grasp why other people might behave towards him in these ways, or feel particular feelings towards him.

> I honestly don't know what interests me more, why Bob doesn't want to recommend me or why I thought Bob would recommend me when he won't. I think the second question has a lot more potential than the first!

Sure, the second question is more interesting, but I don't think this article goes any distance towards attempting to answer it.

People behave in particular ways for reasons that seem apparent to them. The tone of this article annoys me because it appears to suggest that people who behave according to motivations that are hidden from the author are somehow at fault.

I just think this is symptomatic of so many of my experiences within the IT industry - people always assume that their own motives are pure and good, and that everyone else is acting dishonestly (to screw the client, or to avoid doing work, or to advance their own career). I much prefer to assume that if I don't understand somebody's motivations, the burden is on me to try to understand, rather than just writing them off as bad/lazy/dishonest/whatever.

Other than that, I would advise sshing somewhere remote and keeping all of your private project stuff there (i.e. work on it remote - don't keep local copies).

Really, I don't understand the hostility here. Surely this is a worthwhile discussion to have? Either we can establish that it's not a problem that needs fixing, or we can establish that something needs fixing, and identify where it is.

Implying that I'm on some kind of vendetta just because I disagree with you about the source and nature of the flaws in javascript seems a little bit juvenile. These are genuinely-held opinions, and I'd appreciate it if you would not assume that I'm being disingenuous just because I disagree with you.

It's not "odd and bizarre" - it's a belief that the language is fundamentally unsuitable for the things that people insist upon using it for, and reasonably well supported by my own experiences of the language, as well as the reported experiences of others.

> You also don't seem to realize that swapping out js for some other language would mean exactly the same security issues, unless you actually fixed those security issues where they are - in the BROWSER.

I take it you didn't read my reasonably concrete proposals for the use of proof carrying code? It becomes a largely mechanical process to verify that the browser and the language implement "security" in a sensible way at that point.

> If you would like to learn about the language, I'd recommend "O'Reilly Definitive Javascript". Also checkout Rhino.

Thanks. If you would like to learn about Horse and Pony care, I recommend "BHS Complete Horse and Pony Care".

  <script>
  var a = "hello, world";
  </script>

  <script>
  doSomething(a);
  </script>

Once again, I (recursively) refer you to this comment:

http://news.ycombinator.org/item?id=843320

The original article comments may have been talking about a specific community that happens to be called "the theoretical computer science community", hence my point that it is up to members of that community to remember to mentally translate into words that the rest of the universe can understand when talking to people outside their community (which I view as a sub-group of theoretical computer science, for the record).

For some reason you picked up the argument which was only directed at amichail's original comments.

Basically, the framing of the question should actually have read "Are people who go to conference X friendly?" - the actual discussion point was buried in the comments. The question annoyed me, and amichail's even stronger re-statement of this same viewpoint annoyed me further.

And then it just got silly, because now we're arguing about the meanings of words like "many" (my word), or "common" (your word), when really the use of quantifiers in this is really not necessary.

My point was not that there are only a small number of people who use this definition of TCS that I'm complaining about (although I do believe that to be the case) - my point, illustrated with my example about chemistry above, is that it is completely bonkers to use it in this way outside of that community.

http://news.ycombinator.org/item?id=843320

No, it's not, because well-formed, valid Javascript code is permitted to depend on this execution model.

Perhaps, but killing off the stuff that is obviously and demonstrably broken seems like a pretty sensible policy.

That seems like one way of using a sledgehammer to needlessly burn server-side CPU cycles.