Embedded Linux is everywhere. When it comes to building bootable images of Linux-based operating system, there exist popular toolchains such as Yocto and Buildroot. In this post I explore an alternative approach, using a tool known as Nix. The approach is mechanically reproducible and keeps me in the control.
Read more...Robustness and correctness are certainly desirable properties of a piece of software. So is performance. Certain mainstream approaches to robustness, such as dynamic checks, have negative performance effects, which may create the impression that robustness or correstness is fundamentally at odds with performance. But is it really the case?
Read more...TL;DR: Debugging (using a debugger) is painful, unnecessary, and a sign of a poor design.
Read more...In February 1991, a Patriot missile defence system failed to track and neutralise a missile heading towards US Army barracks, resulting in death of 28 people. The report issued by the US General Accounting Office a year later blamed a software error. The growing dependence of our society on software that directly acts on the physical environment (including software in vehicles used for both civilian and military purposes) leads to the question: How do we make safety-critical software more reliable? In this post I discuss an approach to incremental construction of such software, based on a technique known as “refinement”.
Read more...In Minuska, one can describe the semantics of a programming language using term rewriting. As term rewriting is quite low-level and expressing common patterns is repetitive, Minuska, inspired by the K-framework, implements some shortcuts (“syntactic sugar”) whose meaning is defined only by their translation to term rewriting rules. This post motivates the need for and presents a design of a higher-level language-description language that I plan to implement into Minuska.
Read more...I am weighting my options on future research directions.
Read more...Here a present an idea for a simple tool for information flow control. As usually, the idea is language-parametric.
Read more...There is one aspect of the Minuska framework which provides a language designer a great flexibility. Namely, a programming language configuration is a tree whose leaves hold values from an arbitrary domain (typically integers, lists, etc); it is up to the language designer to choose a suitable domain. This makes writing language-parametric tools in Minuska even harder. In this post I explore some arguments for supporting domain-parametricity anyway, discuss the associated problems, and sketch out a possible solution.
Read more...In order to be useful, data stored in computer need to represent real-world phenomena. However, making the representation go through an extra level of indirection – through the realm of mathematics – can be benefitial.
Read more...Debugging is costly. Theorem proving is costly. Debugging by attempting to prove a property that does not hold and then wondering about why it can’t be proven - you do not want to do that. How do I know? I have tried that too many times.
Read more...