“Correctness of a compiler for arithmetic expressions” (McCarthy and Painter 1967) describes the first proof of compiler correctness. To make it easier to play with the proof, I coded it up using the Lean theorem prover.
NB: I came across a survey paper (Zhao, 2011) on some plane geometry problems that a group of friends and I explored around 2000. It’s a nice trip down the memory lane. I played with computer-aided proofs using Maxima recently and thought it might be fun to write down the results.
The IMO Grand Challenge aims to “build an AI that can win a gold medal in the (International Mathematical Olympiad) competition.” Geometry problems are an attractive target (e.g., see this MathOverflow discussion or this Lean’s Zulip stream), given the rich literature on automated theorem proving in geometry.
There are several commonly used RISC-V instruction pairs with 32-bit immediates. Below is an example of loading a 32-bit immediate into a register using lui/addi: lui rd,imm[31:12] addi rd,rd,imm[11:0] Here lui places a (sign-extended) 20-bit immediate into register rd and fills the lowest 12 bits with zeros, and addi adds a sign-extended 12-bit immediate to register rd.
There is a Mars retrograde this year, from September 9 to November 13. Mars appears to move backwards as Earth overtakes Mars. Below is a plot of its positions in the sky using d3.js. It also includes Jupiter and Saturn retrogrades, both from mid May to mid September.
According to NASA, Mars Close Approach this year is May 30 (or wait until 2018). So I re-ran my program from the earlier post Mars or UFO to compute the locations of Mars in the night sky in 2016, including retrograde from April to June, as shown below:
It has been a while since I blogged last time. One change is that I started to have nightmares about me forgetting to prepare for lecture, rather than forgetting to turn in homework as in the past 20(?) years—life does get better.
Stare at the C code below and guess what could go wrong. It’s originally from a CPU simulator, implementing a 16×16⇒32 unsigned multiplication. Thanks to Mattias Engdegård at Intel for sharing the story.
Came across a funny book titled 5000 years of UFOs (1997) last weekend. The author claims that a number of ancient astronomical records from Chinese history books are actually about UFOs. Here’s one example, where the author cites the chronicle Zizhi Tongjian (1084):
A little fun for the last day of 2012: how to crash a program via division? x86’s IDIV instruction traps not only on division by zero, but also on INT_MIN / -1 (signed integer overflow).