A blog about programming, math, education, music, and other things of interest.
- Job offers are welcome
Due to recent events I am heading from academia to RnD and hence open to job offers.
- When functions dissolve
Deconstructing the functions in the soup of assembly code.
- Writing essays
Writing texts was an acquired taste for me. Here I am advicing my former self on how to become a better writer.
- Variance in programming languages
Concepts of variance and contravariance in type systems of programming languages.
- Advice for programming students
What I wish I have heard when I was 18.
- Why every programming student should learn Coq
How playing with automated theorem provers may be beneficial for developing a set of skills which is crucial to any programmer.
- Memory in CompCert: overview
How memory model is described in CompCert, a certified C compiler written in Coq and Ocaml.
- A beautiful intuition on associativity
- On teaching programmers and mathematicians
Some bits of my personal experience on teaching various subjects, specifically related to mathematics or programming.
- The virtues of using goto
gotois marginalized in programmers community which likes the simple one-line recipes for the complex challenges of writing code. In some situations, however, using
gotois the best tool in your box, and I will show you why.
- Proving dependent equalities in Coq with SSReflect
A little trick.
- Causation in modern philosophy of science
Cause and consequences are one of the fundamentals of human reasoning. However, these concepts are based on intuition and lack strictness and connection to the real word. This post is a quick introduction to modern causation from the philosophical point of view.
- Proving type inequalities in Coq
A trick on proving inequalities of types with different numbers of inhabitants.
In the past, the posts were written in a WordPress blog, then I switched to markdown and Jekyll.
Finally, because the Jekyll themes turned to be unstable as the necessary gems get updated, I have decided to switch to
org-mode that I am using daily anyway.
I have to thank Sergey Lebedev and Hervé Grall for influencing this decision.
The current version of this blog is generated by Emacs using
org-publish [ sources ].