Why every programming student should learn Coq

My personal experience with Coq proof assistant over the last years made me think, that such tool, as exotic and niché as it might seem, is invaluable in a programmer’s education. Maybe we should include it in common Software Engineering and Computer Science master programs, so that students prove theorems using it.

Taking notes in markdown: insert a part of a screenshot

I have recently switched to Spacemacs with markdown-mode to write everything markdown-related, especially making notes for whatever things I am fiddling with. While ‘markdown-mode’ is amazing, there is one feature I miss, that is: ‘pasting’ a part of a screenshot into a markdown file by saving it somewhere and generating a correct link. It is a huge waste of time and concentration to do it by hand.

Bigger sphere inside of a smaller one

Can we put a sphere with a bigger radius inside of a smaller one so that it would be fully contained? The answer is yes, but we have to select the space we are working in carefully. I am going to provide two examples here:

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.