rubber duck typing 📇
I write about programming, philosophy, math, education, systems, and music.
Recent posts
- AI could finally let us teach software engineering properly
What junior developers were doing, AI is doing better. What's the point of struggling through learning to write the code by yourself? And what should junior developers do now, and how can we mentor them towards senior roles?
- AI is finally killing IT education for good
AI helps you cheat and it's okay -- the assignments were measuring the wrong thing anyway. The scarce, unfakeable resource was always expert attention.
- Hierarchical multitarget error diagnostic system for ZKSync OS
My purpose-built, multitarget DSL in Rust for rich and actionable diagnostics with verbosity controllable in compile time, built in line with modern system engineering approaches.
- Vico, Descartes, and decay of knowledge in software.
Making is knowing, it makes things intelligible. This is the foundation of epistemology of the Napolitan philosopher Giambattista Vico, and it explains why we lose the knowledge of software faster than it decays technically. I am overviewing Vico's philosophy as a system/software engineer, highlighting connections with our daily work, and raising concerns about AI code generation.
- What is it like to be a man but a bat?
A wizard turns me into a bat, but is there anyone to notice?
- How 4D objects found their way into system engineering
What system engineers learned from philosophers of time and space.
- Challenges of specifying and compiling gas-fueled languages
Gas-metered platforms break the usual compiler correctness rules.
- Argument from recollection in Phaedo is self-illustratory
The argument from recollection in Plato's "Phaedo" displays a clever writing trick, being self-illustratory, and leveraging the dialogue form to convey additional meaning.
- 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)
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.
- Putting a bigger sphere inside a smaller one
In some spaces, smaller spheres can contain bigger ones!
- 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
gotois marginalized in programmers community which likes the simple one-line recipes for the complex challenges of writing code. In some situations, however, usinggotois 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.
Generated by Emacs using org-publish ( sources ).