rubber duck typing
A blog about programming, math, education, systems, music, and other things of interest.
Recent posts
- Compiler correctness
How bugs in compilers are different from bugs in more common programs?
- My note-taking process
A workflow of reading, annotating, and note-keeping.
- Programming languages and computer systems (1)
A first post in a series about computer systems, their design and the role of programming languages.
- Job offers [RnD, compilers, PLT, systems] 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.
- Impressions of René Magritte
Some bits of my personal experience on teaching various subjects, specifically related to mathematics or programming.
- The virtues of using goto
Using
goto
is marginalized in programmers community which likes the simple one-line recipes for the complex challenges of writing code. In some situations, however, usinggoto
is 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.
The first version of this blog was based on WordPress, then I switched to Markdown and Jekyll.
Finally, because the Jekyll themes proved to be unstable as the necessary gems
were updated, I decided to switch to org-mode
, which I was already using daily.
I thank Sergey Lebedev and Hervé Grall for influencing this decision.
The current version of this blog is generated by Emacs using org-publish
( sources ).