A blog about programming, software engineering, and computer science
In the previous post I discussed how LLM affect education in software engineering. We use code assignments with two purposes: to evaluate the students and their studies, and to train them in the engineering. Evaluation was always problematic – proper evaluation targets understanding and reasoning behind a finished program. This requires a one-on-one conversation with a competent mentor, and is not…
The programming education is finally dying for real! It was not the market, the narrow specialization, the corporate pressure, the high level languages (programming without knowing assembly? But you don't know what it really does!), the 234-th Javascript framework, the StackOverflow (Ctrl-C Ctrl-V), the bootcamps (you can learn all you need to know in a week! Quick, start shipping!), or the…
I view my projects through the system engineering lens, employing system and ontological thinking, stakeholder and requirement analysis, complexity management techniques, and so on. When I was working in Matter Labs, I have touched all sorts of things spanning from compiler frontend and optimizations and formal verification to DevEx and system programming. One of my last gigs was designing…
This is the second post in the series dedicated to ontologies in systems engineering: Perdurantism in systems engineering standards 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…
There seem to be at least two problems with the inaccessibility of mental states. First, communication. Our language is a tool to communicate publicly; it has no good words to describe private experiences, the nuances of "what is it like". Bodily sensations give us some grounding, because I can tell you how grief, or sadness, or shame feel in my body; but the richness of my mental states is not…
This is the first post in the series about ontologies in systems engineering: Perdurantism in systems engineering standards Vico, Descartes, and decay of knowledge in software Engineers need a way to talk about the world. They need to agree on what exists, what matters, and how to describe it. For example, making an online shop means automating a part of some organization which has employees,…
In the previous post on compiler correctness we asked: how do you know a compiler has a bug? The answer is surprisingly hard. Most languages have no formal spec. Comparing program behavior is undecidable. Programs may have multiple possible behaviors, or even no specified behavior at all. Even experts disagree on what counts as a bug. Some programs run on platforms where every instruction costs…
Plato impresses me not just with his ideas, but by his writing craftsmanship. In line with his definition of philosophy as a practice, a process, both content and form of his writing contribute to its message. What's said is important, but how it's said adds another layer to the meaning, sometimes illustrative, sometimes adding a twist of depth. In this post I'd like to share some of these…
This post explores the notions of bug identity, bug identification applied to compilers. I will try to highlight why compilers are so difficult to check for correctness. Context: Verification and Validation of Software Model of a program Most programs can be modeled as a black box that reacts to events. In simple cases, the only event is feeding the program input data, and the only reaction is…
I love being efficient and there is nothing like a feeling of wholesomeness at the end of the day when you realize that you have not wasted it. I am not incredibly productive, but I am more productive then some people, including myself for practically my whole previous life. I attribute my recent increase of productivity to my knowledge acquisition system. It is not a perfect system indeed, and…
A couple years ago I have started to write my second book, whose main point is to teach students elements of computer system design, largely speaking. Besides discussing the notion of systems, complexity and approaches to managing systems' complexity in a meaningful way, I want to give special attention to the programming languages. Source code transformed into a running program is an important…
The time has come for me to work in Europe again. For the last couple of years I was residing in Poland and France, but my main occupation was reforming a curriculum for system architects in ITMO university in St.-Petersburg, Russia. Our idea was to create a novel curriculum in Computer Science and Engineering tying together the science of complex systems, programming, computer system architecture…
In this post we are going to explore how the notion of function loses its significance as an abstracted module of program logic when we compile a higher level imperative language to the assembly code. In imperative programming, functions isolate pieces of program logic. For example, in C-like language, the following function would increase its argument by one and return its value. int f ( int x )…
I am not a naturally good writer. It took me writing a 450 pages book and countless pages of notes, reports, essays and posts to only start building a sane mechanism to identify the exact flaws in my writing (and in the text creation process itself). I found an introductory document on writing essays by J.B.Peterson to be of a great use for me. I think it is valuable for someone like me who has to…
Covariance , invariance , and contravariance are concepts many students have difficulties to grasp. However, the idea behind them is pretty simple. This post will attempt to illustrate that in a shortest and simplest way possible. Take an imaginary object-oriented language with generic types. Java or C# will do. We are going to draw diagrams, where rectangles represent types and arrows represent a…
There are many things I wish I knew when I started my journey as a programming student. Almost 10 years have passed since, and, sadly, I can not share my experience or insights with my past self, only with my younger colleagues. This post collects some of the most useful bits of advice I wish I heard when I was 18. Decide who you are You certainly do not need to be familiar with formal logic or…
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. When we are learning to program, we are trying to make a piece of code "just…
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: First example: metric space Suppose we are in a metric space with Euclidean metric. The space is a sphere itself, with radius \(r\). Let us denote a closed sphere of radius…
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.…
I found a beautiful explanation about what essential 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 an element at the beginning of a list is independent from adding something at the end of a list. These actions do…
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…
Recently I've been lucky to spend a couple of days in Belgium. I've come to Bruxelles, rushed through Brugge and Gant and ended my journey by visiting René Magritte museum. I was quite impressed, partly because I have not seen much of Magritte before. This post is intended as a quick review of my impressions and thoughts on Magritte style and his philosophy. First impressions Magritte's style…
IT folks are prone to prejudices, as we all are. Once a beginner programmer starts exploring the world of coding, he quickly learns catchy memes from the more experienced part of the community. One can then easily live by them without putting much thought in their meaning. In general, this is also how human society works: we adopt elements of our parents' lifestyle and their world view, we make…
Proving dependent equalities in Coq is boring, but quite frequently done. I got so annoyed with it that I wrote a little tactic to automatize it a bit. It does use ssreflect routines but it should not be hard to adapt it to vanilla Coq. Ltac depcomp H := apply EqdepFacts.eq_sigT_eq_dep in H; apply Coq.Logic.Eqdep.EqdepTheory.eq_dep_eq in H. Ltac eq_comp c x y := move: (c x y); case; last try do…
Our minds use the notions of cause and consequences all the time. It is, without a doubt, one of the fundamentals of human reasoning. However, when observed closely and formally, it becomes apparent that our concept is based rather on intuition and lacks strictness and connection to the real word. This post is intended as a quick introduction to causation from the philosophical point of view.…
Sometimes you just want to prove that nasty ~ T = U for some types T and U . Well, while in general it is not decidable (nor provable), sometimes there is a relatively easy way to do it, when T and U are not both infinite. In other words, either T or U , or both of them should be finite. Simple example: bool is not unit The idea is simple: if types are equal, there exists a bijection between their…