A blog by John Wickerson
I've used Santander Cycles to get from King's Cross to Imperial College hundreds of times over the last couple of years, and I'd like to think that I'm pretty close to finding the fastest possible route now. The basic route is to aim for New Cavendish Street and then cross Hyde Park, but I've found… Continue reading Cycling from King’s Cross to Imperial College London
Yann Herklotz has added hyperblock scheduling to his verified high-level synthesis (HLS) tool called Vericert, and I'm very pleased that our paper about this work has been accepted to appear at PLDI 2024 this June. This paper was our "difficult second album", in the sense that we'd already published a paper about the first version… Continue reading Verified high-level synthesis – now with hyperblocks!
The Hoare triple $latex \{P\}\,c\,\{Q\}$ has a very simple meaning, namely: $latex \forall\sigma, \sigma'\ldotp \sigma \in P \wedge (\sigma,\sigma') \in c \longrightarrow \sigma'\in Q$. That is: if the precondition $latex P$ is satisfied in some state $latex \sigma$, and $latex c$ can transform $latex \sigma$ into $latex \sigma'$, then $latex \sigma'$ must satisfy the postcondition… Continue reading What is the other Incorrectness logic?
The world of computer architecture is quite excited these days about something called Compute Express Link (CXL). It's a new standard that allows the various components of a datacentre computer to communicate large amounts of data efficiently with each other. In this article, I'll explain what CXL is, and why there is so much excitement… Continue reading CXL: What’s all the fuss about?
I've commuted via King's Cross St Pancras to Imperial College's South Kensington Campus for about a decade now, but have only recently discovered what I believe to be the fastest possible route between those two London stations. King's Cross St Pancras to South Kensington takes me about 20 minutes, and the return journey takes about… Continue reading The fastest route between King’s Cross St Pancras and South Kensington
When writing multi-word adjectives, hyphens can be important. But many writers use either too many or too few. This blog post is my attempt to clarify the situation (as I understand it). The basic issue is that "adjective noun noun" can be hard for readers to parse. The default is to understand it as (adjective… Continue reading Hyphenation: when and why?
My friend and colleague George Constantinides wrote an interesting post on his blog recently where he formalises St Anselm's argument for the existence of God. Since I'm teaching a course on the Isabelle proof assistant this term, I thought I'd see if I could recreate that argument using Isabelle. Here goes... theory God imports Main… Continue reading Proving the existence of God using a computer
A little old lady worked all on her own On a paper about a result she had shown. A wise old man heard her grumble and rage: "There’s not enough room on my page! Wise old man, won’t you help me, please? My paper’s a squash and a squeeze."
FCCM 2022 in New York City has just drawn to a close, so I thought I'd put down some thoughts about my experience while it's fresh in my mind. As my first in-person conference since covid, my expectations were sky high, and I'm very pleased to report that my expectations were well and truly met… Continue reading Some reflections on FCCM 2022
When playing the board game Cluedo (also known as Clue in North America), you make a series of hypotheses that consist of a murderer, a weapon, and a room. In each hypothesis, the room has to be the room your piece is currently in, and the player to your left always has the first opportunity… Continue reading The “Cluedo” effect in randomised testing
Wickopedia 