I was away in Sydney at the end of last week for a NICTA workshop on Formal Methods. The venue was the Scientia building on the UNSW campus. I had a pleasant three days, gave a talk that prompted some interested sounding questions, and heard lots of interesting talks by others.
As is often the case at these sorts of gatherings, there was a bit of soul-searching about the utility of what we’re doing. Carroll Morgan put it nicely when he said that we shouldn’t be too harsh on ourselves, and that FM suffers a little from the same problems as AI, the perception that
If it’s not boring, it can’t be Formal Methods.
The problem is that academic theory takes a long time to filter out into industrial practice (and not all theory is going to make it either, of course; some of it’s no use to man nor beast). Someone working on theory now may well have to wait an awfully long time in order to see their work gain a broader acceptance. And given the failure rate, how can they be sure of its real worth?
Finally, my last word on The matrix:
This article analyses the film from a religious and/or philosophical point of view, and finds all sorts of interesting stuff in it. This is all very well though I can’t help suspect that you’d find all sorts of interesting stuff in just about anything if you looked hard enough, and if you knew what you were going to find in advance. My problem with The matrix is more that it’s poor science-fiction, and any amount of religious imagery doesn’t alter that.
On the other hand, it is an entertaining film.