Memory in CompCert: overview
CompCert is a certified C compiler written in Coq. I work with it to create a verified refactorer, that is proven correct w.r.t. operational semantics of C. During my journey, I am tackling various parts of CompCert, including its memory model. It might seem interesting, how they dealt with raw memory and handled things like encoding values.
There were several versions of memory specification. This note is describing the second version, as of CompCert 2.6. Some minor details are omitted for brevity (like alignment checks); I will probably make more posts about memory and connected subjects. But first we have to take a look at Radix trees, a data structure pervasive in CompCert.
A beautiful intuition on associativity
I found a beautiful explanation about what property does the associativity capture: You can think of each element of a monoid as having two sides. The idea is that the left side and right side are independent things that don’t interfere with each other. For example, adding some stuff at the beginning of a list, and adding some stuff at the end of a list, don’t affect each other, and it doesn’t matter which you do first. That’s the idea that associativity captures.
On teaching mathematics -- a summary of Kudryavtsev's book
I’ve recently read a book of L.Kudryavtsev, a widely known mathematician. He was the head of maths department of Moscow Institute of Physics and Technologies, and an author of course books on mathematical analysis. The book title is roughly translated as “The Principles of Teaching Modern Mathematics”. This post is intended as a collection of advices and thoughts I’ve picked from there.
On teaching programmers and mathematicians
I have been lucky to be exposed to some very good teachers with different approaches as well as collect my own experience: I am teaching C/Assembly since around 2009. I’ve also taught things like Lambda-calculus and functional programming, mathematics and playing piano. This post is intended as a summary of how I see an ideal education in virtually any domain. I will speak about teaching mathematics and or programming; the principles however are sufficiently abstract to be applied anywhere.