My summer has started in great style, with a week-long trip to take part of the Vienna Summer of Logic – which the organizers describe as “the largest event in the history of logic”.
It was really a fantastic event, with dozens of conferences and workshops which are usually spread over summer, brought together in one place over a 10-day period. It was all quite overwhelming, with days with over 25 parallel sessions, but a great opportunity to broaden the mind and explore some of the rich branches of this subject. There were logicians, philosophers, mathematicians, computer scientists… and through this rich variety it was possible to see the common themes uniting these fields.
Too many things to remember and process, so I am writing here just some of my thoughts.
For me it started in an odd way: within my first few minutes I realized I was in the wrong room! I had planned to be in a systems biology workshop but I quickly realized I wasn’t – I could have made a hasty and clumsy exit from the room and a clumsy entry into another one or just stay put. I did the latter, and was rewarded with an excellent session on some things that I had never heard of before. This in fact was a constant theme for me: moving from workshop to workshop, or conference to conference, and learning new things. The large number of parallel sessions meant that there were many talks I was interested in but couldn’t go to, but overall I felt my time was well spent.
The main discovery for me was the variety of flavours of formal logical systems that are being explored. Terms which started to make some sense to me: nilpotent logic, reversive logics, relevance logics… Some talks really concentrated on specific results by authors and which went right over my head, but some stand out as attempting to explain intuitive ideas to justify a shift away from what is known as just “classical logic”. In particular, the tutorial to explain Łukasiewicz logic was particularly good. Some of the introduction to non-standard logics happened outside formal sessions, which is where in particular I learned about paraconsistent logics, which seems to be specifically of interest to many Brazilian logicians.
***This paragraph is a very very short intuition for some of the non-classical logics, hopefully useful to any reader who has no idea what I am talking about: In general, logic allows us to reason about some property, say P, and its negation, say notP. Usually we assume that one and only one of P and notP have to be true, so our initial assumption is that P or notP is true, and that P and notP is false. Some of the non-standard logics allow us to question these two rules, or tautologies. For example, if we assume that P or notP is by default true, then it allows us to prove something by case analysis: if we can show that Q is true when P is true, and we also show that Q is true when notP is true, then we have essentially shown that Q is always true–but one could argue that this is cheating, like hedging our bets. However, in logical systems where we remove the tautology that P or notP is true by default, then if we prove Q we really have a much better intuition of why Q is true; such logics are usually called intuitionistic logics. On the other hand, we have the tautology which says that P and notP cannot ever be true. The problem is that we may actually need to reason about domains where there is a certain amount of ambiguity – so a world where P and notP are both true is not absolutely inconsistent but… paraconsistent. And so it goes – these are just some of the arguments to explore non-standard logical systems.***
Anyway, VSL allowed me to think about some of these issues, and start to see formal logics not only from the very pragmatic point of view of verification but also from a more nuanced, philosophical view. However, the verification aspects were also well represented, and there was plenty of evidence of the progress in the development of theorem provers. I was impressed that both Isabelle and Coq are now extremely polished and sophisticated systems, with powerful automation and speed to be able to tackle large verification tasks. I do feel a bit nostalgic for the old days when users of these systems knew exactly the nitty-gritty of the implementation – that is, how logical inferences were represented in the underlying programming language, typically a flavour of ML. Now, users interact at a much more abstract level, and take a lot for granted. I assume this is similar to early programmers going on about their 8-bit computers that allowed them to really know what was going on, as opposed to these sleek black or silver boxes called mobiles which do a huge amount of processing as if by magic. I confess to being an old fogey of the theorem proving world. But I need to move on with the times and I talked to very friendly developers of both Isabelle and Coq who encouraged me to get back into using proof systems. Watch this space.
I went to Vienna with my Synthetic Biology hat on and went to several talks relevant to this. I was very impressed with the work done by Thomas Henziger’s group where they are starting to look not only at genetic networks in an abstract sense but also studying the effects of changes to promoter sequences- but as it became clear, the state space becomes huge and iti very difficult to extend the use of model checkers to realistic scenarios. I will also be following the work of Joelle and Amy in developing a logical framework for systems biology. Microsoft Research continues with its great work on providing tools for reasoning about biological systems, with unfairly professional cool animations and high quality implementations. I hadn’t followed the area of DNA computing before, so it was excellent to go to several talks where researchers are developing clever ways to exploit the physical properties of DNA, namely the specific bonding between pairs AT and CG and the creation of strings of nucleotides, to create interesting systems, even including “gel-lular automata”!
I could go on, but I am sure I have lost most of my readers by now. I still need to follow up some of the leads from the many talks.
Apart from the talks, there was a great social vibe in Vienna, and I got to meet up with friends and colleagues I hadn’t seen in many years. Well worth attending this unique event! And Vienna is gorgeous, of course, and I hope to visit this beautiful city again.