Four short links: 29 May 2017
Formal Correctness, Conversational Maxims, Learn Datalog, and AlphaGo Retires
- An Empirical Study on the Correctness of Formally Verified Distributed Systems (Paper a Day) — the formal verification ensured the protocol was bug free. By far, the biggest group of bugs relates to assumptions about the behaviour of components that the formally verified system interacts with. These bugs manifest in the interface (or shim layer) between the verified and non-verified components. Buffers, escaping, incomplete reads, unreliable communications, all tripped them up.
- Google’s Three Secrets to Designing Perfect Conversations — One secret to making sure that line one leads to two, and two leads to three, comes from James Giongola, creative lead on conversation design and voice direction at Google. He recommends that chat designers take advantage of the rules baked into the Cooperative Principle, a concept created by British philosopher Paul Grice in the 1970s. Grice theorized that people employ all sorts of norms (which are known as Grice’s Maxims) to make sure that conversations flow normally. These maxims serve as simple hacks for anyone writing robo-conversations—the key is to make sure your bot is always offering enough information to keep a conversation going.
- Learn Datalog Today — Learn Datalog Today is an interactive tutorial designed to teach you the Datomic dialect of Datalog. Datalog is a declarative database query language with roots in logic programming. Datalog has similar expressive power as SQL. Prolog as a query language, more or less, designed to parallelize, so popular with the Big Data kids. This is gentler info than reading the Datalog papers.
- AlphaGo “Retires” — DeepMind will release the data from 50 games of the AI playing against itself for the Go community to study. DeepMind is also working on a teaching tool based on AlphaGo to be released sometime in the future. Ke Jie will collaborate with DeepMind on the tool, which Hassabis says should give “all players and fans the opportunity to see the game through the lens of AlphaGo.” I certainly hope this happens. It seems cheap to pop up and win the title, then retire and never play again. IBM’s Deep Blue team did this after their software beat Kasparov. If it means the humans never get to learn how to beat the software, then this feels like the engineers using the game rather than loving the game. If you loved the game, you’d leave the game better than you found it rather than unsettled and unresolved.
