Engineers vs Logicians

This past week I was attending a summer school about software verification, called VTSA, in Saarbruecken. There were many interesting lectures and I could learn much about model checkers and SAT solvers, giving me very good impression of the event.

From a more proof-theoretic and automated deduction perspective, it was interesting to see what is researched in model checking and in SAT solvers. They seem to do more engineering oriented research, trying to have good implementations and algorithms to overcome the state space explosion when modeling always more complicated softwares; while we try to work more in expressiveness of the logic and postpone, as much as possible, to implement specific algorithms that can handle some specific cases. So there is a contrasting approach in the communities: the theorem proving employes more logicians, while the model checking community employes more engineers.

However, I was very impressed on how far the engineers/model checkers/SAT solvers can go by "hacking" logic to be efficient. They seem to have many more applications cases than the automated theorem proving community, and seem to attract more and more the attention of industries. The negative aspect is that the size of software models seems to be growing much faster than the computational power of computers, what implies that more "hacks" would be necessary to obtain efficient implementations, and with these "hacks" more mysterious these systems would be. Moreover, the properties that we would like to be proved also tend to be more expressive, and hence may not be possible to check them by using model checkers at all. Therefore, I believe that in the future there will be an increasing demand for theorem provers, and to meet this demand, we must research more logic. This does not mean, however, that model checkers will not be used any longer. I believe that for simple properties, model checkers will continue to be used in larger scale, as proving with model checkers is in general easier than with theorem provers.

Modern Person?

Recently, Andrea brought to my attention a very curious way of Indians classifying a person as a modern person, what is not at all common in the western world. For an Indian, modern people are those that do not wear traditional Indian clothes, and that are more flexible towards traditions, such as dating or flerting, enjoying the nightlife, and other more "western" habits. As Indian society has not yet freed itself from religious/traditional habits, specially those traditions related to relationships before marriage and women suffrage, this classification is normal in India, but long forgotten in western cultures, where these movements happened one or two generations ago. That was indeed a very curious observation of cultural differences affecting language.

Working Holidays? Why work?

In the past three weeks, I was traveling through Australia, passing from Sydney, Alice Springs, in the center, and Cairns, to the east coast. As I was traveling alone, I prefered to stay in hostels, where is easier to meet people and enjoy more my stay. I met people from several nationalities, Germans, lots of them, French, Dutch, etc. What surprised me the most is that they are not ordinary backpackers, as those that we see in Europe and travel around for maybe 1-2 months. They were the so called Holiday-Workers, people that obtain a special visa and that are allowed to work, usually in blue collar jobs, and stay in Australia for longer periods, visiting the country. Though the idea seems interesting, I still did not understand why is this a good option, compared to the alternative of working in Europe and only then coming to Australia for a shorter period.

Each time I met one of these working-holiday students, I would ask why they do not just come for a short period, only for vacations. I obtained different answers: some would say that they come for the culture experience, what is not very convincing, since the Australian culture is not that different from the European and, moreover, with the jobs they do and the places they stay, they meet more Europeans than Australians; others said that they came here to save money for passing their universities later. What is also not very satisfying, since the living cost in Australia, specially the hostel rates, are very high, and I really doubt that the get some money out of this trip, when considering that they have to pay an expensive flight ticket.

I think the real reason for them to come here in hoards is a more basic one: independence. These holiday-workers are students that just finished their high school and are eager for "freedom" from their parents. They are constantly partying and getting wasted. What brings me to my point. Why work in Australia? Isn't it better to work in Europe and make short holidays there itself?