Prof. Haritsa's views on research

I recently bumped upon this interesting link on Prof. Jayant Haritsa's views on research. Although it is supposed to be Prof. Haritsa's views on MS vs PhD, much of it discusses his views on research life in general. As he says in the beginning, he is heavily biased towards a traditional notion of academics.
I don't think I have enough experience to comment on this topic. The last part is worth quoting:

Finally, in my view, ideal Phd is one where *you* come up with the problem, work alone (modulo advisor) and single-handedly write a definitive thesis on the issue.

Still considering grad school?

P.S. My personal interaction with Dr. Haritsa was primarily during the DBMS course he offers. Highly recommended if you end up at IISc!

Perlis' epigrams

Alan J. Perlis was the first Turing award winner, "for his influence in the area of advanced programming techniques and compiler construction". He is also famous for his article Epigrams on Programming, which contains 130 one-liners, mostly about his experience with programming. A few of the epigrams are on epigrams... he calls them meta-epigrams (Russell's paradox?)!
Five pearls I found from the article (go dig your own):

• A language that doesn't affect the way you think about programming, is not worth knowing.
• There will always be things we wish to say in our programs that in all known languages can only be said poorly.
• The computer is the ultimate polluter. Its feces are indistinguishable from the food it produces.
• Computer Science is embarrassed by the computer.
• The last epigram? Neither eat nor drink them, snuff epigrams.

Geeky quotes

Thanks to Sumit for the link.

---

Here is a link to a bunch of (funny and/or insightful) programming quotes. Some of them are by well known personalities, but some are from Anonymous blah blah.
My favorite:

Debugging is twice as hard as writing the code in the first place. Therefore, if you write the code as cleverly as possible, you are, by definition, not smart enough to debug it.
Brian W. Kernighan

Telling an SMT solver to tell them apart

Thanks to Jacob Burnim for this post.

---

A few days back, I was trying to write a sudoku solver using an SMT solver. The idea is to express the constraints of a sudoku board in a language that an SMT solver can understand. The solver either gives a model from which the solution can be extracted or it declares the constraints to be unsatisfiable in which case no solution exists.
The SMT solver I was using was Yices. I first used the following assertion to tell Yices to make all the values in a column distinct:

(define-type single_dig (subrange 0 9))
(define board::(-> single_dig single_dig single_dig))

(assert
(forall (n1::single_dig n2::single_dig m::single_dig)
(or (= n1 n2) (/= (board n1 m) (board n2 m)))
))

Neat and compact! But wait... when you give it to Yices, it cowardly backs off, returning unknown! OK, fine, too many quantifiers... lets ask it to do it for each row separately. But no... still no luck! Notice that the subrange we are working on is finite, but somehow Yices fails to understand that. After trying many different expressions with quantifiers, I gave up (Yices is really bad with quantifiers).
And then came Jacob with a smart trick. Just define a function that maps the board values to different integers:

(define f::(-> single_dig single_dig))
(assert (and
(= (f (board 1 1)) 1)
(= (f (board 2 1)) 2)
(= (f (board 3 1)) 3)
(= (f (board 4 1)) 4)
(= (f (board 5 1)) 5)
(= (f (board 6 1)) 6)
(= (f (board 7 1)) 7)
(= (f (board 8 1)) 8)
(= (f (board 9 1)) 9)))

And voila! It automatically makes all board values distinct. Yices does not complain any more. Of course this is not too compact and the model returned by the solver becomes a bit clumsy, but it works! Looks like this is a standard trick to make a finite number of values distinct.