Blog about computing and truthing. About the search for the essence of computing. About understanding the essence of knowledge. And some other interesting stuff, technical and not that technical.
Correctness properties of programs are traditionally decomposed into safety (“nothing bad happens”) and liveness (“something good eventually happens”). In sequential verification, this corresponds to the well-known decomposition of total correctness into partial correctness and termination. In this paper, we present a principle-first view of correctness: under suitable safety guarantees, liveness…
On June 29th, in St. Louis, MO, USA, the C++ standard committee voted to include P2300 std::execution in the upcoming C++26 standard. The result is now published in the C++ standard working draft . A short introduction to this can be found in Herb’s post . As expected by many, the plenary vote was controversial. I wrote this post to share some of my thoughts on the subject. Are senders/receivers a…
In this talk I make a critique of Inheritance as it is present in mainstream OOP. We look from multiple points of views on the Inheritance relationship, and we show that, at a closer inspection, it doesn’t reach up to the promises it makes. The talk touches the simple problem of the Rectangle and Square , it discusses the parallel with the is-a relationship, and it shows how the Liskov…
Based on Language Unlimited: The Science Behind Our Most Creative Power book by David Adger, in this Overload article I tried to explore how programming languages should be built, taking a linguistic perspective. The main idea is that we might hope that programming languages are structured in such a way that, reading the code can be done without any effort, leaving the main cognitive powers to…
In my last Overload article, I was arguing that the senders/receivers models may be a bit too complex. Soon after writing it, I realized that this is just perceived complexity. One can change the perspective at looking at the same proposal, and with that change of perspective, the concepts may be simpler to understand and work with. Moreover, the model seems to be strong enough to use it as a base…
Executors are one of the most expected features for the upcoming C++ standards. This article tries to cast a critical perspective of some of the main proposals discussed for adoption. Besides briefly explaining the content of the executors proposal and providing a few examples, the article tries to pick on some decisions made in those proposals. It tries to argue about the strong and the weak…
C++, like most imperative languages, have a bad tradition in writing multi-threaded applications. Concurrency safety ranks first in terms of C++ development frustration (far ahead from the second place). This talk shows how concurrent C++ applications can be designed by shifting the focus from low-level synchronisation to a set of concurrency patterns that deal with higher-level constructs. The…
Lately, we often compare the time spent reading code versus the time spent in writing code. And, we somehow lump together the actual reading of the code with reasoning about the code. But, if we look closely, these are very different activities. We discuss too much about reading code but too little on what it means to reason about code. This article tries to explore a few aspects of what it means…
Composition and decomposition are probably the most important tools we have as software engineers. And yet, for multi-threaded programs that use locks and raw threads, composition and decomposition doesn’t properly hold. This article tries to consider composition and decomposition of task systems, showing that task systems play nice with regards to those two. As with most of the later articles,…
Similar to gotos, raw threads and locks should be banished from day-to-day programming. Moreover, we have far better way to build concurrent applications. Watch my ACCU 2021 talk to see more. Video is available on YouTube . Slides and more information can be found here . The session first introduced nolocks.org , which I hope helps in spreading the word that locks should be avoided. Keep truthing!