Functions aren’t ready for Assembly

Inspired by https://drewdevault.com/2019/02/18/Generics-arent-ready-for-Go.html.

In the distance, a gradual roar begins to grow in volume. A dust cloud is visible over the horizon. As it nears, the shouts of the oncoming angry mob can be heard. Suddenly, it stops, and a brief silence ensues. Then the air is filled with the clacking of hundreds of keyboards, angrily typing the owner’s opinion about functions, calling conventions, and Assembly. The clans of Algol, Cobol, Fortan, C, Forth, Lisp, and more – usually mortal enemies – have combined forces to fight in what may become one of the greatest flamewars of our time. And none of them read more than the title of this article before writing their comment.

Continue reading

Modelling Rolling Deployments in Alloy

Introduction

This post has a few goals. One is to outline how to think about a simple imperative process in a declarative language/system like Alloy. Another is to make a case for why this kind of formalization is a worthwhile exercise for software engineers.

Disclaimer: To get the most out of this post you need some familiarity with Alloy syntax otherwise most of it will probably not make much sense. I’ll try to explain things as I go along but promise no mind blowing revelations. As some old person used to say, “There are no royal roads”.

Continue reading

Individual Comfort

This is a response to

By being declarative and deterministic, and rendered in ordinary plain text, HTML and CSS conceal no surprises, which is likely why they are not considered “real programming” by “real” programmers. This property, however, makes them especially easy to learn. Moreover, they are all you need to learn in order to achieve a great many useful results in an open Web.

https://doriantaylor.com/googles-long-march

Continue reading

Learning Trick: Gamification

One really cool trick I’ve discovered over the years is gamifying the learning process. Instead of doing a linear pass through some learning material I approach it in a non-linear fashion and take various detours by asking dumb questions and taking them to their logical conclusion. The downside is that it’s somewhat more time intensive than a linear pass but the upside is it’s more fun and I seem to retain the information better.

Practical strace: Retrofitting Build Caching

If you look at a build process abstractly then it is basically a function that uses some files as inputs and creates some files as outputs. We can peek into this input/output process with strace by invoking the build script with strace and then asking it to log all file operations. After we recover the inputs and outputs we can retrofit a caching mechanism on top of the build process by hashing the inputs and using that as a key to save the outputs.

To make things more concrete I’m going to use a simple script as a stand-in for a build process

Continue reading

Portfolio Theory of Code/Systems

Most people agree that code is a liability. The more code you have the worse things get because more code means more entropy and more problems from emergent and unanticipated behavior. So most people agree that the less code you have the better. In this sense TDD is doing the wrong thing because TDD is just more code. Formal methods on the other hand are not code and they de-risk the code portfolio by offloading parts that would be code into something that is not code and hence not a liability.

So really what I’m saying is that if you want to reduce risk associated with code then invest some time in learning formal methods and how to utilize formal methods instead of code to specify and validate systems.

Oblique Note on Methodologies

In all optimization problems the solutions must incorporate the biases of the objective function otherwise they are sub-optimal solutions and will be beaten by solutions that exploit more of the structure/biases inherent in the objective function. Evolution works iteratively on short timescales and as byproducts/solutions of the evolutionary objective function we incorporate the short term biases/structures inherent in evolution. I think this means long term thinking and planning is fundamentally a doomed enterprise for organisms like us and if you want to be rich and famous then appeal to the here and now.

This is why I no longer think agile is a good way to develop software. It’s impossible to do any kind of longer term planning and work with an agile methodology. More specifically, any kind of long term thinking will not survive in an agile environment because it won’t exploit the planning structures inherent in the agile process.

Variation of the Pigeonhole Principle

In math, the pigeonhole principle states that if n items are put in m containers and n is greater than m then at least two items must go in the same container. This principle is formalized in “Software Foundations” as follows

Theorem pigeonhole_principle : forall {X:Type} (l1 l2:list X),
  excluded_middle ->
  (forall x, In x l1 -> In x l2) ->
  length l2 < length l1 ->
  repeats l1.
Continue reading