22 June 2020

I hope everyone had a good Midsummer weekend!

[Somerset] Our weekend was a bit on the rainy side, but we got out to Dundon Beacon a couple of days later to commune with nature. Given how pretty and how full of wildlife it is, it's surprising how few people you encounter on a typical walk there. It has winding paths through ancient woodland, clearings with rope swings, unspoilt meadows full of butterflies in the summer and a viewpoint on the Iron Age fort hilltop from which you can see lots of Sedgemoor.

I spent much of the last week preparing for moving. My living room is now stacked with crates, ready to go off to storage. Dave has reported that one of my honey bee colonies need to be moved to a bigger home, so in between the packing I've been putting together DN4 brood frames for them.

I also had quite a few thumping headaches last week, prompting me to give up caffeine. I love coffee, and it seemed that over time I had been making it stronger, and stronger, and stronger. I was up to nearly a gram of caffeine on some days, really quite a lot. Cutting back wasn't much fun but I'm feeling a lot better now and sleeping a lot better too!

[Go] Another — less delibilitating — addiction that I've been attempting to manage this week is Go. My third game concluded in a win for me, but with two stones of handicap (really quite a lot!) I learned a few things. Last week I talked about my inability to recognise false eyes. Within the game, in a practical setting, I learned the difference between the lines in the opening, and I learned to spot the formation of common eye shapes. Chris wiped out masses of my terrority with a single carefully-placed stone, which was pretty cool. The analysis with KataGo consistently recommended the same intersection for both of us, over a fifteen-move period, so that'll be something to go over in review! It's like the AI was screaming at us to play there and not be distracted in our local fight elsewhere.

As I write, my fourth game with Chris is in progress as well as a fifth with Fergal following a call on Twitter and Mastodon. I've dug out an ancient Android tablet I used to use and installed an OGS app on it so that I have a dedicated device for sitting and playing electronic go games in the garden or on walks without notifications popping up, or the temptation to surf the web, or other distractions. Our Wednesday night group has a few ladders to play in — 9×9, 13×13 and 19×19 board sizes are available. If you're reading this, it's likely that you know me, so join us, if you'd like.

As well as this, I've switched my main go study book to Cho Chikun's Go: A Complete Introduction to the Game. I really like this one so far. Like Learn Go, it teaches partly through example games, in a nice informal style. However, it doesn't lose focus from some central concept the chapter is trying to teach — the first six chapters cover an introduction, how to capture, eyes and living groups, kō and opening, for example. Little essays between chapters on the culture of go enrich the beginner's understanding of the game. Go for Beginners by Iwamoto Kaoru is another much-loved beginner's book. I've ordered it too, it's on the way now and I'll post my initial thoughts next week.

I've also been introducing Tim to the game via our regular chats on Signal. For this I hacked up a bit of horrid Perl to make diagrams of the board. As we'd chat, I'd upload a simple diagram and explain to him some concept in the game, or we'd just play a game, making a sequence of diagrams to represent the state of our goban in response to the coordinates of intersections we'd decide on. Over the week, I developed more and more features and then integrated it into my website generator, which now efficiently inlines the images right into pages as well-compressed data URL-encoded PNGs.

So, now I have a way to easily produce diagrams in my pages. Here are some examples from last week:

Tim's first game, a 7×7 atari go game that he's currently winning convincingly as Black.
Tim's first game, a 7×7 atari go game that he's currently winning convincingly as Black.
The victim of a ladder sees it reach its deadly conclusion.
The victim of a ladder sees it reach its deadly conclusion.
A deadly strike on a bulky five shape by White.
A deadly strike on a bulky five shape by White.

[Haskell] It's surprising how enjoyable writing diagramming code can be. Perhaps it's because the results are immediately noticable. The results of tweaks or new features can be appreciated concretely and visually. Several weeks ago I heard the January 2014 episode of the Haskell Cast in which Brent Yorgey talks about his then-new package developed with a new philosophy to declarative drawing, diagrams. Part of the philosophy is that diagrams are modelled as monoids under the action of superimposing diagrams to combine simpler ones into more complex ones. The library aims to be principled, building diagrams elegantly from a simple set of primitives, specifically trying to get away from the world of hacked-up scripts which themselves output code to generate a diagram in something like PGF/TikZ or PSTricks.

Anyway, as he talks about diagrams you hear him going between talking about composing diagrams from specific kinds of objects to (the philosophy/design of) the implementation. Later, when talking about education, he talks about the hurdle of his course's students of being able to move between different levels of abstraction without getting them mixed up, which is very important in computer science and maths. For example, implementing the monad instance for an arrow, and programming with that monad abstraction. And I get why writing diagramming code is fun. You're switching between making some specific diagram of interest, tweaking the objects which comprise it, and improving the overall program so you can make it more flexible --- all the time getting immediate visual feedback to inform aesthetic and functional choices.

Speaking of Haskell, I've rather neglected the feeding of my interest in this in the last fortnight. Maybe it's because other diversions like games like go feel like more of a pick-up-and-put-down activity to relieve the monotony of packing. But I hope to get back to the machine learning and functional programming work this week, especially as I've been chatting to Tom on email. Hacking away on this stuff can make days disappear for sure, but for now, I have to get the potentially stressful stuff out of the way before I get back to the fun. Having said that, I imagine it's like learning a new natural language — half an hour every day is better than working all weekend once a month. I should try to remember that.

He recommended I read Kleene's Introduction to Metamathematics, a tour of first-order logic — the foundational stuff, mathematical logic and recursive functions, as well as the computability of functions and Gödel's incompleteness theorems. This looks like the kind of book which could help me revise and re-internalise a bunch of stuff I should know, and introduce me to some stuff I'd like to.

[Coq] Tom works with Coq and Isabelle, both interactive theorem proving environments. They help the user in writing a a mathematical proof that's verifiable by a program. They are typically used not only for formalising mathematics but also for verifying and certifying computer programs and programming languages. This formal verification concerns the proof of whether an algorithm conforms to a formal specification or other property.

The Curry-Howard correspondence is a mapping between logics (which talk about things like propositions and proofs) and type systems (which talk about things like types and functions). The two seem different in how they operate, but they actually follow similar rules. This correspondence is the core idea of Coq. Coq can be viewed as a logical system which acts as an assistant in the checking of proofs of supplied assertions, finding formal proofs, and extracting programs. Coq can also be viewed as a programming system, a dependently-typed functional programming language based on a higher-order type theory.

A typical Coq programmer's workflow is firstly to define the necessary data structures, the objects and their properties, then to write and prove the intermediate lemmas, building up to the main theorems, then to extract the program — certified correct and hopefully efficient — from the proof (as Haskell, OCaml or Scheme). Equivalently, a functional programmer will implement the functions — usually with very expressive dependent types — and prove that the functions meet some desired specification. So, either way, the programmer is developing a proof (a program) with supplied tactics guiding the process. And in defining a term, you can either supply a type or definition, or just specify the type and try to search for a proof of it. Cool.

And that's the extent of what I know about it so far. Being about logic, type theory and functional programming, Coq seems worth trying out. Sometime in the next few weeks I hope to dive in with a combination of Mike Nahas's Coq Tutorial and Coq in a Hurry, both listed on the Coq documentation page.