Nixie Clock Project 2017-09-24

I have had a few sets of Nixie tubes lying around for a while, waiting for a use. I bought them on ebay with the plan of eventually building a clock out of them. I had entertained the idea of designing my own Nixie clock PCB, but I finally decided to buy a kit instead. I purchased the Nixie Clock QTC IN-14 kit from PV Electronics. It was fun to solder the kit and the finished clock is beautiful. I love the look of Nixie tubes – they have a very nice warm glow.

Here is a time-lapse video I made of me soldering the kit:

I drew the clock case in FreeCAD. The sides of the case were cut from acrylic sheets and the corner brackets were printed on my 3D printer.

No Comments on Nixie Clock Project
Categories: Uncategorized

Making Tools 2017-09-18

In The Mythical Man-Month, Fred Brooks describes his vision of an ideal software engineering team, called The Surgical Team. In this team, there is a dedicated toolmaker to help the lead programmer/system architect. The Surgical Team model hardly exists in practice nowadays. Instead, a software engineer is expected to fill multiple roles, including toolmaking. In my opinion, toolmaking is an essential skill for any productive programmer.

In my experience, it feels very fulfilling to building a tool to improve my workflow or solve a specific problem or need. I love programming because I love to solve problems, and building small tools is like an easier kind of programming with faster feedback. You also avoid a lot of the bureaucracy that comes with building a full application: writing tests, issue tracking, writing documentation, building releases, and so on. These things can be added later if the tool will be shared with others. However, I often make tools just for myself, and that simplifies the development process and makes it much more fast and fun.

When I think about programmer tools, I group them into three categories: simple one-off scripts, complex command-line applications, and GUI tools.

One-off Scripts

The most common type of tool that programmers build are small single-purpose scripts to perform a simple but repetitive task. Typically these small scripts are used to perform file-oriented tasks like batch renaming of files, uploading files to a server, or parsing data from a file and converting it into some other format.

Terminal emulators have simple scripting functions built-in so that you can compose scripts in a single command line. These are known as one-liners, and they often appear in Stack Overflow answers and tweets. There is even a website dedicated to Bash one-liners.

Simple scripts are great for automation. By using cron, you can make certain things happen at regular intervals. For example, I use cron scripts to regularly update websites when I commit to certain repositories. I also use cron to water my plants.

Command-line Tools

The natural evolution from a one-off script is to make a more complicated command-line utility. One of the main distinguishing factors is that command-line tools usually take input arguments, whereas a script usually does not.

A command-line tool may be a more reusable version of a script, that fits a more general purpose. In other cases, a command-line tool is used to solve more complex tasks that require much more code.

Interpreted languages like Python are popular for making command-line tools because they enable fast prototyping. With Python, you can test your tool without first compiling it. Python also has a REPL that allows testing small pieces of code quickly.

Here are some examples of tasks I have solved by making command-line tools:

  • Converting Markdown to HTML with additional template expansions.
  • Automated benchmarking for various applications.
  • Software release automation.

GUI Tools

Command-line tools can be very useful, but they are not ideal for data entry. Data can be provided to a tool via data files in a readable format, like JSON. However, for a tool that requires lots of user input it is often better to build a GUI for the tool. This enables modifying the input without restarting the tool.

It is not easy to build a GUI, especially if you are not familiar with a GUI toolkit. It may pay off in the long run to learn a GUI toolkit just to be able to build interactive tools for yourself. Simple web applications can work as a great platform to make tools with GUIs.

I often use JavaFx to build tools that require editable input. It is not the easiest toolkit to learn, but I use JavaFx in Chunky so I didn’t learn it specifically to make tools for myself. It works well for me because I prefer to use Java for most of my projects. Building tools in the same language makes it easy to integrate with the rest of the project.

I’ll show some examples of tools I made using JavaFx. The first one is a profiling tool:

This tool collects execution traces from a network socket. The data is displayed in interactive graphs, so that I can zoom in on interesting regions. The tracing data comes from applications that I want to profile. The tool helps me identify which parts of the applications take most time. The graphs give a great overview of the runtime behavior of an application.

The most recent GUI tool I made was a 3D model editor. I built this for Chunky development. In Chunky, all block models are made up of quadrilateral surfaces that are coded manually in Java. The spacial and texture coordinates of each surface must be precisely specified for it to render correctly. This works fine for simple models, but it becomes cumbersome for more complex models. For example, this is part of the code for the lever model:

The first, probably obvious, problem of using this format is figuring out which coordinates to plug in to the code. The second, and less obvious, problem is that I often have to restart Chunky to see what effect a change has. This takes a long time and is especially annoying when making tiny changes. It’s easy to get something wrong and have to tweak it multiple times, causing multiple restarts, to fix a problem.

To improve rapid prototyping I made a render testing tool that makes it easier to construct these 3D models in Java. The tool was written so that it could efficiently use hot code reloading in IntelliJ to reload code changes in a running instance of the tool. This helps a lot in building new models, but it was still very tedious to define 3D models manually in Java code. I usually resorted to drawing models on paper first to figure out the coordinates I needed.

Recently I was working on adding armor stand rendering, and I decided to build an interactive model editor to help with the modeling process. Here is a screenshot from the current version of the model editor:

The model editor is a great help in building new models, because I can immediately see the spacial relation between blocks and it takes away much of the tedium of manually defining quadrilaterals. The geometry in the editor is block-based, so the six individual faces of each block are automatically generated based on the parameters of one single block. Texturing the faces is also significantly easier using the tool, since I can directly see if any texture coordinate is incorrect.

No Comments on Making Tools
Categories: Uncategorized

Learning Coq 2017-06-29

I recently read the free book Software Foundations by Benjamin Pierce. The book starts by introducing basic proof theory and logic. In later chapters programming language topics like Hoare logic and type systems are taught. The Coq Proof Assistant is used in all examples and exercises in the book. In fact, the whole book consists entirely of Coq scripts written in a literate programming style.

Part of my motivation for reading the book was to learn how to use Coq. By solving all the examples I now feel pretty confident in using Coq to construct proofs for simple theorems.

Since this was the first time I have used a proof assistant, I thought I would share my thoughts about learning Coq.

Using Coq

It took me a long time to learn how to use Coq efficiently. The exercises in Software Foundations do a great job of introducing one small concept at a time and then practicing it in many different ways. The exercises do take a long time to solve, but I thought it was very fun to solve them. Each exercise consists of proving a theorem. It feels extremely rewarding to finally complete a difficult proof that took a long time to solve.

I got addicted to solving Coq exercises. Some exercises took me more than a week to solve. Some exercises kept me up late at night, because I could not stop thinking about them. To me it seemed like solving Coq exercises was very similar to solving puzzles in The Witness. The kick I got out of solving an exercise was very similar to the kick I got out of solving puzzles in The Witness, or other puzzle games.

The term “Proof Assistant” is deceptive. You get no assistance in figuring out how to prove properties by using Coq, however the tool assists you in checking that the proof is correct. This can be a huge help because you can be sure that you have not made a mistake, that the proof really proves what the theorem states. When I write an informal proof I always worry that I might have made a simple mistake that is not apparent to myself on inspection. This worry is erased almost entirely when using Coq. Instead, you only really have to check the theorem to see that the property being proven is actually the one you wanted to prove.

When I got deep into working on a proof, I sometimes lost track of what I was trying to prove, and how the particular subproof I was working on related to the overall theorem. It was very useful to sometimes take a break and try to think through everything from the high-level theorem again. Sometimes it was very useful to illustrate small examples on paper.

One of the exercises in Software Foundations that I found most difficult was the exercise to prove the pigeonhole principle. I was very happy with my proof when I finally completed it, so I tidied it up and published the proof on GitHub. My solution does not use the principle of the excluded middle, which is much more difficult than the version you have to prove in the original exercise.

Functional Programming

Part of learning Coq is to learn the programming language used to write proofs. The language, Gallina, is a very advanced dependently typed functional programming language. Most concepts are familiar if you have already programmed in a functional language, which I had. The part I had most difficulty with was the way inductively defined types are declared and used in induction and case analysis.

Some aspects of functional programming can be very difficult to work with if you are mainly used to imperative programming languages. The exercises on church numerals were the most difficult for me.

Proof Theory

I was not confident in my ability to write mathematical proofs before reading Software Foundations. I am now much more confident that I can prove simple theorems. I think this is mainly due to working through the exercises in the first six chapters of the book. These chapters introduce general techniques used to construct proofs.

The most important concepts in mathematical proofs are direct proof, case analysis, and induction. I had learned a bit about these concepts from my undergraduate studies, but I developed a much more systematic way of using them by working through the exercises in the intro chapters of Software Foundations.

Type Systems

The later parts of the book become very advanced, but it was easier to work through the exercises after becoming familiar with Coq.

After the introduction to proof theory, logic, and functional programming, Software Foundations continues on to Hoare logic and type systems. Some of the exercises are about proving that simple programs work according to some specification. A system for constructing such proofs in a systematic manner is introduced in the Hoare logic chapters. The chapters on type systems are all about proving that a well-typed program always makes progress (does not crash).

This was the first time I have read about type systems and Hoare logic. The book seemed to give a good introduction to these topics. I really enjoyed the exercises that were about constructing correctness proofs for simple programs.

The best thing about the book is that all the exercises can be run in interactive mode in the Coq IDE, to see how everything works. This made it fun to read the chapters about type systems.

1 Comment on Learning Coq
Categories: Uncategorized

Uninteresting Code Metrics 2017-05-25

I was browsing the GitHub repository rapid7/metasploit-framework and noticed that the README displayed a “code climate” badge. The badge displayed a number of unknown significance: 2.7.

It was clear from the name that the badge had something to do with static analysis. Clicking on the badge leads to this page:

Yikes! 3694 seems like a pretty large issue count. It leads me to believe that the developers either don’t care about their Code Climate score (but then why would they display the badge in the README?), or that they don’t find the Code Climate issues useful.

During my first internship at Google I worked on the static analysis team. One thing I learned from the team was that static analysis findings are only useful if they are actionable and have a low false positive rate. This paper from the team lists these as the first two requirements for selecting static analyses:

I looked at the issues Code Climate reported for the repository in question, and it seems Code Climate is reporting mostly non-actionable issues regarding code complexity. The other type of issues are duplicated code. I looked at several of the reported duplicated code fragments, and they were all pretty simple code blocks with no more than five lines, and most had only two occurrences. The duplicated code issues seemed nitpicky.

Complexity Score

Code complexity metrics (including line counts) are not useful for fixing real problems in code. If you try to enforce some maximum complexity you will end up with pointless rewrites just to try to fix the complexity score. This in itself can lead to needless bugs being introduced from trying to “fix” your complexity issues.

Another issue is that the complexity score in itself is entirely arbitrary. What does it mean that a method has a complexity of 300? Is that too much? Where do you draw the line? If you make the computation of the complexity score more sophisticated, it just gets more difficult to figure out what part to change to minimize the score.


Sometimes it can be useful to find that some replicated piece of code can be refactored into a common method. However, this often leads to introducing a more abstract method that handles more cases, increasing your code complexity. Often, a new parameter is added to the method, and some conditional statements as well. Consider for example Figure 1 from Narasimhan (2015):

In my opinion the above refactoring is not useful. The more general method will run slower than the original method due to the new conditional branch, unless it is inlined by the compiler. The more general method is also harder to read and has introduced a boolean trap.

No Comments on Uninteresting Code Metrics
Categories: Uncategorized

Voxxed Days Zürich 2017 2017-04-30

In February I visited Zürich to give a talk at a software developer conference called Voxxed Days Zürich. The event was very fun, and I’m thankful to the organizers who invited me to give a talk.

My talk was about a Java compiler, ExtendJ, which I have been working with extensively during my PhD studies. My PhD subject is declarative compiler construction with Attribute Grammars, and ExtendJ has been very useful as a platform for my research projects. I have used ExtendJ both as a testbed for programming language experiments and as a benchmark for Reference Attribute Grammars.

The goal of my talk at the Voxxed Days event was to show some of the cool features in ExtendJ. I also wanted to briefly show some of the aspects of the design of ExtendJ that are interesting or unusual compared to most other compilers.

The slides from my talk are available here. The presentation was recorded and can be watched via YouTube:

No Comments on Voxxed Days Zürich 2017
Categories: Uncategorized

I am Not Scared of the AI Singularity 2017-03-10

One common idea when discussing the future of Artificial Intelligence (AI) is that, if humans ever develop an AI that reaches above some threshold of reasoning power, then the AI will increase its own reasoning power and become progressively “smarter” until human intelligence pales in comparison.

The following quote is from the synopsis of Nick Bostrom’s Superintelligence on Wikipedia:

[…] once human-level machine intelligence is developed, a “superintelligent” system that “greatly exceeds the cognitive performance of humans in virtually all domains of interest” would follow surprisingly quickly, possibly even instantaneously. Such a superintelligence would be difficult to control or restrain.

This idea, that there will exist a type of AI singularity, if we just develop an AI that is “smart” enough, is attractive but naive. With our current technology, I don’t believe that type of scenario would be possible.

Let’s destruct the idea a bit. My interpretation of the core hypothesis is this:

AI Singularity Hypothesis
If there is an AI running on a processing unit, and the AI is intelligent enough to take control of other processing units, it could take advantage of those other processing units to increase its own computing power and thereby increase its own intelligence.

The hypothesis assumes something I think we should not take for granted: namely that adding more computing power will necessarily increase reasoning power.

One of the main problems in large-scale computations today is communication. Many interesting computational problems are bottlenecked not by the available computational power, but by the communication latency between processing units. Some problems can be solved in parallel trivially because they require no communication between processing units, all other problems are fundamentally more difficult because you also need to handle communication efficiently. Communication is needed to share partial results between the participating processing units.

Superintelligence <-> Supercommunication

I believe that superintelligent AI is not trivially parallelizable, and that it in fact requires a high degree of communication between processing units, hence it will be bottlenecked by communication. This is of course speculation, but you should not assume that the opposite is true either, which is what the AI Singularity Hypothesis is based on.

If communication is the bottleneck for superintelligent AI, then it won’t help to spread the computation over more processing units. That would increase the amount of communication needed, working against the bottleneck. What you need instead is a very compact processing unit with very fast, short-distance communication.

Consider the human brain. It is a very dense network of highly interconnected neurons. It seems like the ideal structure for highly communication-intensive computation. This might be an indication that human-level reasoning requires a lot of communication. It is hard for me to imagine that human-level reasoning would not require huge amounts of communication.

I am of course just speculating about AI here. I am not an expert in this field, I have merely written a few simple machine learning applications in my spare time. However, I felt like I had to voice my opinion because it always annoys me when people take it for granted that an AI with higher-than-human level intelligence would automatically become all-powerful.

2 Comments on I am Not Scared of the AI Singularity
Categories: Uncategorized