Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
gdp
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
10 ms
·
61.
▲
by
gdp
17y ago
I seriously hate these lists. Top 100 universities at doing what? There's no point being in the crappiest department of the "best" university.
62.
▲
by
gdp
17y ago
Well, the main thing would be to operate in a store-nothing kind of way. There has to be a fixed amount of storage required no matter what the length of the input is. You'll need to keep aggregate totals and compute over each row, as oppo
63.
▲
The bug-free myth: Why we trust verified software
(plsadventures.com)
1 points
by
gdp
17y ago
|
0 comments
64.
▲
by
gdp
17y ago
I don't think I understand the question. Are you actually asking how to read from a terabyte flat file, or are you asking how to process a terabyte of sequential data? They are two (related) but distinct questions.
65.
▲
by
gdp
17y ago
No, I wasn't suggesting you were disagreeing, I was simply responding to your hypothetical disagreement that some might argue. My counter-argument could be just as applicable to any of the people who have professed similar beliefs to the o
66.
▲
by
gdp
17y ago
> Some may argue that there's no guarantee that such proofs apply to real world systems. 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
67.
▲
by
gdp
17y ago
For this project, that's assumed. Provided you have some kind of formal semantics, you can define translations. And in fact, Adam Chlipala's work on certified compilers show that it's not impossible. http://adam.chlipala.net/papers/CtpcP
68.
▲
by
gdp
17y ago
I was using 'assumption' in the strict mathematical-logic sense. These assumptions are stated and it is trivial to check that the proof is not true if the assumptions aren't true.
69.
▲
by
gdp
17y ago
Read the link. 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 tha
70.
▲
by
gdp
17y ago
http://news.ycombinator.com/item?id=760547 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
71.
▲
by
gdp
17y ago
As has been said before, it's not about being "bug free" - it's about a number of safety properties always holding as long as the assumptions are true. The safety properties might be things like who can write to what memory, and when it is
72.
▲
by
gdp
17y ago
Extrapolating the effort involved in proving huge numbers of complex safety properties for an operating system written in C to programs in general is a bit silly. Doing formal verification in more abstract languages gets considerably easie
73.
▲
Insecure software is your fault
(plsadventures.com)
2 points
by
gdp
17y ago
|
0 comments
74.
▲
by
gdp
17y ago
Somebody who repeatedly sends invites and then calls is not going to get a recommendation from me. If you are actually worthy of recommendation, people will probably do them with very little encouragement. Hounding people for recommendatio
75.
▲
by
gdp
17y ago
OK, perhaps I didn't phrase my objection very well. > 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 justifi
76.
▲
by
gdp
17y ago
I think it's actually relatively easy to figure out what people think about you. If you do something, and a number of people react, you can generally start to draw a "trend line" through the behaviours of different people towards you over
77.
▲
by
gdp
17y ago
I didn't do anything except post here, so I assume it's a feature of that blog.
78.
▲
by
gdp
17y ago
Wow. I don't know if it's just a literary device being employed here, but this article comes off as the work of somebody with a lack of empathy. Through the description of the actions of each of the people with whom he disagrees, I immedia
79.
▲
by
gdp
17y ago
This basically seems like a table to compare attributes of languages that are much less different from each other than they are from everything else. I don't think it usefully captures any attributes that people actually care about.
80.
▲
by
gdp
17y ago
Keyloggers are unlikely to be particularly useful in this case, but if you imagine you are being keylogged, then you can take appropriate steps to mask your behaviour. Other than that, I would advise sshing somewhere remote and keeping all
81.
▲
by
gdp
17y ago
You appear to be relying on the clairvoyant abilities of those you correspond with. My example could be re-factored into exactly the same situation you're talking about by substituting the body of each script tag with two files that contai
82.
▲
by
gdp
17y ago
> You seem to have something odd and bizarre against the language. 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 suppo
83.
▲
by
gdp
17y ago
We're entitled to wishful thinking. Wishful thinking gives us something to aim for, and then we can evaluate in realistic terms how far towards that goal we can get.
84.
▲
by
gdp
17y ago
You have chosen a particularly strange definition of "code". <script> var a = "hello, world"; </script> <script> doSomething(a); </script> My program is either syntactically invalid (because
85.
▲
by
gdp
17y ago
Given that I object to the use of Javascript outside of browsers, you've basically negated (for me) any reason to treat the issue of language security versus browser security separately.
86.
▲
by
gdp
17y ago
I'm really not trolling. The only reason I started arguing this point is that it was with some irritation that I saw the suggestion from amichail that the definition of "Theoretical Computer Science" excluded theoretical computer scientist
87.
▲
by
gdp
17y ago
I'll refer you to this comment now, as we appear to be arguing about the same thing in two threads: http://news.ycombinator.org/item?id=843320
88.
▲
by
gdp
17y ago
> Javascript is an innocent bystander in the mess. No, it's not, because well-formed, valid Javascript code is permitted to depend on this execution model.
89.
▲
by
gdp
17y ago
Don't you think that something that prevented people from unintentionally introducing XSS vulnerabilities into their code would actually be easier ? Building broken software is always easy, so shouldn't we be focusing on making it easier
90.
▲
by
gdp
17y ago
But there is lots of code that relies upon that behaviour. We can argue about the exact source of it if you like, but if the language execution model is dependent on that behaviour, then the language execution model is flawed, which was my
More ›