Talk Review: A Pictorial Introduction to Separation Logic

Dr. Tony Hoare is a clear and precise speaker. Attending his talk is a great experience.

In this talk, the speaker talks about a new logic that unifies the concepts of pointers, concurrency, weak memory and communication. The speaker starts by defining four degrees of separation between two program traces: 1) they are disjoint traces 2) one is sequentially after another 3) both of the traces can be executed in parallel 4) both the traces are mutually exclusive - they cannot happen together.

It is then seen that 4) => 3) => 2) => 1) - that is, the relation 3) holds whenever 4) holds, 2) holds whenever 3) holds and so on.

"Hoare triples" are then introduced. These are related to the concept that post-condition are true when precondition and invariant of a program are true. The triples can be composed in interesting manners.

Though I did not understand much of what follows because of these results, through google search it seems that these results are useful in proving program correctness. The next day Dr. Hoare presented a topic related to program correctness in another conference.

Presentation slides are here (only about half could be covered in his talk). Further reading keywords: Galois Connections (pdf, pdf), Category Theory, Event Algebra.

Talk Review: Internet Pioneer Vinton Cerf

Vincent Cerf talks about the future of internet and the world.

1. India and China will have very large internet population and economies by 2035. Fresh water and energy would be more precious than today.

2. Collaboration on the internet creates many new opportunities - like early discovery of epidemics using medical queries made by people on the internet. Real time data will be much more useful and available.

3. People will travel a lot less for office and virtual interactions will be much more real.

4. Much more kinds of devices and individual contributions are enabled by the internet. Devices will be more intelligent.

5. Much more efficient and managable computers will be used in cloud computing. Processes can have unique identifiers which enables them to transfer from one computer to another.

6. Work on interplanetary internet using new protocols is in its initial phase.