dougws

This is a pretty good blog post (based on a really good paper) that describes the fundamental differences between interpreters and compilers: http://blog.sigfpe.com/2009/05/three-projections-of-doctor-f...

You've just invented the field of program synthesis, which is a super active research area right now in programming languages! Here's the paper list from a class at UW focused on this area: http://courses.cs.washington.edu/courses/cse599a2/15wi/ . The Sumit Gulwani paper from the first week is a really good introduction to the field.

Speaking from academic computer science, I have never heard of anyone making the decision not to work on something for this reason--perhaps because if an idea could immediately be turned into a successful company, it's probably not good research! And most (all?) CS PhD programs (which include an MS in passing in the USA) guarantee full funding for a number of years and most successful students are funded the whole time.

You absolutely shouldn't feel "mentally inferior" to folks with PhDs. Doing academic research, which probably involves getting a PhD, is almost certainly the best way to make a significant contribution to Computer Science. These two facts aren't really in conflict, I don't think.

One could imagine doing some kind of differential testing of another key-value store against vard to ensure that for a random but large number of requests, they return the same value. I'm not sure that doing that would gain you anything over using Jepsen [1], though. One could also imagine implementing another key-value store in Verdi and proving it equivalent to vard; reasons to do this might include using better data structures or serialization mechanisms, or a different consensus protocol. I'm not sure that this would require significantly less effort than proving this new key-value store (usrd? whittend? :)) correct from scratch, but I'd love to see someone do this!

[1] https://github.com/aphyr/jepsen

At this point, the standard intro text is Software Foundations [1]. I highly recommend it; it will teach you Coq and also probably make you a better programmer. After SF, Certified Programming with Dependent Types [2] gets more into the practice of proving serious programs correct. These books are both available online in the form of literate Coq files.

As far as online lectures, OPLSS [3] often has Coq lectures which are quite good.

[1] http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

[2] http://adam.chlipala.net/cpdt/

[3] https://www.cs.uoregon.edu/research/summerschool/summer15/

Thanks! Let us know if you have any questions about the proof itself--unfortunately, it's not particularly well-documented, and Coq isn't super easy to read in the first place.

We are reading! This is a great question. We currently don't prove anything about liveness. We'd love to work on this.

As you probably know, Raft and other consensus algorithms are not guaranteed to be live in all situations. But subject to some assumptions about the frequency of failure, they are guaranteed to make progress.

In Verdi, systems are verified with respect to semantics for the network they are running on. Our semantics currently don't include any restrictions about how often failures can happen; a failure "step" can occur at any time. We're not sure what the best way is to introduce this kind of restriction, but we've got a couple ideas. One would be to guarantee that the total number of failures has some finite bound which is unknown to the system itself but which is available during verification. Another would be to model failure probabilistically. We will probably end up doing at least one of these things in the next year or so :).

Hey, I'm Doug Woos--thanks for this excellent summary! It's worth noting that the Raft proof was completed by a team of people, including me, my research partner James Wilcox (http://homes.cs.washington.edu/~jrw12/), and the other folks listed on our web page at http://verdi.uwplse.org/

Investigating theft takes up police time, which expends taxpayer resources. The market wouldn't take this into account.

Also, "doesn't California have bigger issues to worry about" is just silly, as if the government of an enormous state can only do one thing at a time.

Your objections to MongoDB's model seem reasonable, but I don't see any evidence in either this comment or the linked blog post that DocumentDB is better (especially in the absence of benchmarks). What is this "battle-tested distributed systems framework"? Several of your complaints about MongoDB have to do with the interaction between persistence to disk and replication to the network; as the Multi-Paxos algorithm does not specify when data should be written to disk (much less what the format should be), what reason is there to believe that DocumentDB does this any better?

I'm totally willing to believe that DocumentDB beats the pants of MongoDB on just about every axis (in fact, that seems pretty likely) but it's going to take some actual numbers and a better description of the internals.

Seems like this is pretty comparable to Vagrant using the Docker backend. Anyone have thoughts on pros and cons of each?

Did you read the whole article? If not, go ahead and read the part about pressuring the intern into giving his assistant oral sex while he (Kennedy) watched. That is absolutely not "normal behavior".

Last I checked, GIT_DIR wasn't actually respected by a lot of git subcommands. Is that no longer the case?

Maybe give some usage examples in the README? This sounds interesting but I'm still pretty confused about what exactly the program does.

Have used all of the techniques in the article (plus dict/set comprehensions) but had never heard of dict views [1] until now. Good stuff!

[1] http://docs.python.org/2/library/stdtypes.html#dictionary-vi...

I don't see the programming language set. Is it one of the ones that shows up on the front page?

Github's project pages present a really nice, standardized, easy way to find out what a library does. I am always relieved when I find out that a 3rd-party python library I want to use is hosted on github, as it means I can very easily read the documentation, browse the source code, and examine outstanding issues.

Seems like it's likely to be very difficult for a browser to detect whether or not a given request is idempotent, no? You could use HTTP verbs (i.e. assume that GETs are and POSTs are not) but then you're trusting the server to use REST correctly.

I've got two conflicting viewpoints on this article.

On the one hand, I got my current job (as one of the first 10 employees at a startup) by "traditional" means--I saw a job ad, responded to it, interviewed, and accepted the offer. It worked great.

On the other hand, I am now on the other side of the process, and I really wish more people would follow your advice. Enthusiasm goes a really long way--if you're competent and likable, I will likely vote to hire you if you seem enthusiastic. Sending individual emails and doing company-specific prep for your interview should be a no-brainer. Have enough confidence in your technical chops (or non-technical jobs, I guess, if you're non-technical) to put effort into the other aspects of your job search.

Absolutely right. There are plenty of ways of making the same point without invoking a very serious condition that makes a lot of peoples' lives extremely difficult.

This is absolutely true. Market validation goes both ways! Don't assume a product is either viable or unviable without confirmation from the intended consumers.

Please re-read the article--the author is absolutely not making the point you think he is. All he is saying is that hackers are less likely to be willing to pay for software than most people, so the fact that the typical hacker news reader is unwilling to pay for something doesn't mean that it isn't a viable product. It's a shame that the top comment on this article is attacking a straw-man argument.

Feynman story is neat, but it's being used by a rabidly sexist man[1] in an attempt to prove a false point using anecdotal evidence.

[1] http://pechorin2.wordpress.com/2012/05/08/women-shouldnt-hav...

Email with a "+" sign still not working as of 12:00 Wednesday morning.

How on earth did you end up with that impression? While it's true that it's possible to pick up the material on your own, it's the rare individual (I know one) who is actually able to do so completely--and I think this particular guy would say that he would have been much better off had he studied it in school. Teaching yourself CS (and by "CS" I definitely don't mean "building a website in PHP") is really, really hard, and learning it from an expert (in college we call them "professors") is a much more efficient way to go about it unless you're so overwhelmingly brilliant that it's easy for you.

Yes, clearly you have to relearn everything you know about computer programming now that a new version of PHP has arrived.

Computer science != Theoretical computer science.

Most well-written functional programs I've seen actually look like your examples--or rather, the very top-level does. The rest of the code is devoted to telling the language enough about your domain that it's possible to express your goals.

There seems to be a really heavy bias towards relatively new SF; is this because there are more awards now than there used to be, or because you only have data going so far back?