Industrial Programming Languages and Pragmatics

The approach of applying pragmatics and principles of industrial programming language design to formal methods, verification, and dependently-typed languages is something I care a great deal about.  It’s the focus of my programming language project Salt, and it was the subject of my recent lightning talk at IEEE SecDev and many of the discussions that followed.

Those who interact with me know I tend to talk about this subject quite a bit, and that I have a particular concern for the pragmatic aspects of language design.  The origin of this concern no doubt comes from my time with the Java Platform Group at Oracle; there I saw the issues that a successful industrial language must confront firsthand and the demands that arise from real-world industrial use.   I’ve also seen these sorts of issues in other places, like working on the FreeBSD and Linux kernels.

A common question I get is “what do you mean by ‘industrial language’?”  I see this frequently in the context of the academic programming language and Haskell communities.  I’ve seen this frequently enough that it’s prompted me to write an article on the topic.

Academic and Industrial PL

In my experience, there’s something of a gulf between academic knowledge about programming languages and industrial knowledge.  Academic PL is primarily concerned with things like semantics, idealized language features, and type systems (particularly type systems).  Academic PL knowledge is available through the usual academic conferences: POPL, PLDI, OOPSLA, ICFP, and the like, as well as various books and journals.

Industrial PL, by contrast, is generally less structured and accessible in its knowledge, existing primarily in the form of institutional knowledge in organizations like OpenJDK and others dedicated to maintaining major industrial languages.  Some of this makes it out into industrial conferences (Brian Goetz, the Java language architect has given a number of talks on these subjects, such as this one).

In recent history, there has been a concerted effort by the industrial PL world to tap into this knowledge.  This manifests in recent and upcoming Java language features as well as in languages like Rust which incorporate a number of advanced type system features.  I saw this firsthand in my time on the Java Platform Group, and particularly in the work that went into the Lambda project and is now going into the Valhalla project.

Academic PL, on the other hand, has tended to be dismissive of the knowledge base of industrial PL as it lacks the kind of formalism that modern academic PL work demands.  The source of this, I believe, is rooted in the differing goals and scientific foundations.  The concerns of academic PL are well-addressed by higher mathematics, where the concerns of industrial PL are better answered through disciplines such as organizational psychology.  In truth, both are important.

It is my belief that both worlds need to make an effort to get out of their silos.  The industrial PL world needs to do a better job at describing the problems it solves and reporting its solutions and findings.  The academic PL world needs to acknowledge the intellectual merit of creating real-world realizations of the idealized features presented in academic PL conferences.

Principles of “Industrial Programming Languages”

A first step towards getting out of the silo is to clearly express what the notion of an “industrial programming language” means.  This phrase is an example of what might be called a “common-sense” term.  Any of my colleagues from OpenJDK certainly could have expounded at length as to its meaning, industrial programmers could probably list a number of examples, and even academics have some notion of what it means (often some variation on “icky details we don’t want to deal with”).

The problem with “common sense” notions is that everyone has their own ideas of what they mean.  To effectively study an issue, we must refine such notions into more concrete and unambiguous ideas.  A truly principled effort in this direction would, in my opinion, be worthy of peer-reviewed publication.  My goal here is merely to begin to explore the ideas.

As a first draft, we can list a number of issues that “industrial” software development must confront, and which “industrial” programming languages must provide tools to address:

  • Very large codebases, running from hundreds of thousands to tens of millions of lines of code
  • Long-running development, spanning many development cycles and lasting years to decades
  • Very large staff headcounts, distributed teams, staff turnover, varying skill-levels
  • Withstanding refactoring, architectural changes, and resisting “bit-rot”
  • Large and complex APIs, protocols, interfaces, etc, possibly consisting of hundreds of methods/variables
  • Interaction with other complex systems, implementation of complex standards and protocols
  • Need for highly-configurable systems, large numbers of possible configurations
  • Large third-party dependency sets and management thereof

The common theme here is unavoidable complexity and inelegance.  It is a well-known fact in many disciplines that different factors emerge and become dominant at different scales.  In algorithms and data structures for example, code simplicity is often the dominant factor in execution time at small scales, asymptotic complexity dominates at mid-scale, and I/O cost dominates all other concerns at large scales.  Similarly, with software development, certain stresses (such as the ones listed above) emerge and become increasingly important as the scope of a development effort increases.

Industrial practice and industrial languages aim to withstand these factors and the stresses they produce as development scope scales up to modern levels.  An important corollary is that the failure to provide mechanisms for dealing with these factors effectively limits the scope of development, as has been the case throughout the development of industrial practice.

Dealing with Development at Scale

I routinely use the term “industrial pragmatics” to refer to the various methods that have been developed in order to cope with the stresses that emerge in large-scale software development.  In particular, I use the word “pragmatics” because the efficacy of these techniques generally can’t be effectively evaluated using theory alone.  They involve both complex interactions at scale as well as human behavior- two phenomena that defy theoretical abstraction.

It is worth exploring some of these techniques and why they have been so successful.

The Path of Least Eventual Cost/Pain

At very large scales, the only successful strategy for managing things quickly becomes the path of least eventual cost (or for the more blunt, pain).  A key word in this is eventual, as it is critically important to realize that some decisions may minimize short-term cost or maximize short-term gain in some way but eventually lead to a much higher cost in the long run.  At large scales and in long-running projects, short-sighted decision-making can dramatically increase the eventual cost, to the point of compromising the entire effort.

This is, in my opinion, one of the critically-important principles of industrial pragmatics.  Any tool, technique, language, or practice must be evaluated in terms of its effect on eventual cost.

Modularity and Interfaces

More than any other technique, modularity has proven itself invaluable in managing the complexity of industrial-scale software development.  The most widely-successful adoption of this technique came in the form of Object-Oriented programming, which removed the barriers that prevented software development from scaling up.  Since the advent of OO, other adaptations have emerged: Haskell’s typeclasses, various module systems, and the like, all of which share common features.

A key features of these systems is that they manage complexity by encapsulation- walling off part of a huge and complex system, thereby limiting the concerns of both the author of that component as well as the user.  This significant limits the set of concerns developers must address, thereby limiting the size and complexity of any “local” view of the system.

Constraining Use

Large systems quickly build up a huge number of interfaces and configurations, and the fraction of possible uses of those interfaces and configurations that represent “valid” or “good” use quickly shrinks to the point where the vast majority of uses are incorrect in some way.  Well-designed systems provide mechanisms to restrict or check use of interfaces or configurations to identify misuse, or else restrict use to the “good” cases in some way.  Badly designed systems adopt an “anything goes” mentality.

An prime example of this comes in the form of cryptographic APIs.  Older crypto APIs (such as OpenSSL) provide a dizzying array of methods that can result in an insecure system at the slightest misuse.  This problem was identified in recent academic work, and a series of new crypto APIs that restrict use to correct patterns have been created.  Type systems themselves also represent a technology that restricts usage, greatly constraining the space of possible cases and greatly improving the degree to which a program can be analyzed and reasoned about.

Managing Implicit Constraints

In a sufficiently-large system, a significant effort must be dedicated to maintaining knowledge about the system itself and preventing the introduction of flaws by violating the implicit logic of the system.  Well-managed systems minimize the externally-facing implicit constraints, expose APIs that further minimize the degree to which they can be violated, and ensure that the unavoidable constraints are easily detected and well-known.  Badly-designed systems are rife with such implicit constraints and require expert knowledge in order to avoid them.

This is one area that I believe formal methods can make a huge impact if adapted correctly.  There are many ways of approaching this problem: documentation, assertions, unit tests, and so on, but they are all deficient for various reasons.  Even the ability to explicitly codify invariants and preconditions would be a considerable boon.  More modern languages and tools such as Rust and JML approach this, but only formal methods can provide a truly universal solution.

The Art of API (and Protocol/Standard) Design

The design of APIs is an art that is underappreciated in my opinion.  It takes considerable skill to design a good API.  It requires the ability to generalize, and more importantly, to know when to generalize and when to hammer down details.  It requires the ability to foresee places where people will want to change things and how to make that process easy.  It requires a good sense for how people will build upon the API.  It requires a good sense of necessary vs. unnecessary complexity.  Lastly, It requires a knack for human factors and for designing things to make doing the right thing easy and the wrong thing hard or impossible.

Managing Failure

Failure of some kind becomes unavoidable at large scales.  Software systems subject to real use will eventually be used incorrectly, and it will become necessary to diagnose failures quickly and efficiently.  This is unavoidable, even in a perfect world where all of our own developers are perfect- users and third-party developers can and will do things wrong, and they need to be able to figure out why.  In the real world, our own developers also must diagnose failures, if only in the internal development and testing processes.

This, I think, is one of the most undervalued principles in both academic and even industrial circles.  Far too many people want to answer the problem of managing failure with “don’t fail”.  But failure can’t be avoided or wished away, and failing to provide tools to quickly and effectively diagnose failure translates to increased cost in terms of development times, testing times, and diagnosis of failure in the field (in other words, much more eventual cost and pain).

In my own career, Java and other JVM languages have proven themselves to have the best track record in terms of easy diagnosis of failure of any language I’ve seen in common use, both with myself and with others.  By contrast, languages that don’t provide the kind of functionality that JVM languages do, either because they can’t (like C), or because they choose not to (like Haskell) tend to slow things down as it takes longer to diagnose issues.  Lastly, I’ve also dealt with some truly nightmarish platforms, such as embedded or boot-loaders, where diagnosis is a task for experts and takes considerable effort and time.

Human Factors

In addition to the principles I’ve discussed thus far, human factors- particularly the difficulty of modifying human behavior -plays a key role in the design of industrial languages.  A considerable amount of thought must go into how to influence user behavior and how to get them to adopt new techniques and methodologies, often with little chance of recovering from mistakes.  Unlike the other principles, these are rooted in psychology and therefore cannot be the subject of the kinds of mathematical theories that underlie many aspects of PL.  They are nonetheless critical to success.

Making it Easy to be Good/Hard to be Bad

One of the most successful principles I’ve learned is that of making it easy to be good and hard to be bad.  This means that “good” use of the tool or language should be easy and intuitive, and it should be difficult and non-obvious how to do “bad” things (this of course presupposes an accurate notion of good vs. bad, but that’s another discussion).

An excellent example of this comes from the language Standard ML.  Functional programming with immutable data is the notion of “good” in SML, and imperative programming with mutable data is strongly discouraged.  It’s tolerated, but the syntax for declaring and using mutable state is gnarly and awkward, thereby encouraging programmers to avoid it in most cases and encapsulate it when they do use it.  Java and other languages’ design reflects a notion of object-orientation being “good”, with global state being strongly discouraged and made deliberately difficult to use.


Coordinating human activity at scale is an extremely difficult problem.  Regimentation- creating common idioms that serve to make behavior predictable and facilitate implied communication is a very common technique for dealing with the problem at scale.  In the context of software development, this takes the form of things like design patterns and anti-patterns, well-defined interfaces and standards, style documents, and programming paradigms.

Languages that succeed at large-scale development tend to provide facilities for this kind of regimentation in one way or another.  This incidentally is one major argument in favor of types: they provide a considerable amount of implicit communication between developers and users of an interface.  Similarly, languages with well-known idioms and built-in usage patterns tend to produce more coherent codebases.  Java is one example of this.  Haskell is quite good in some ways (such as its typeclasses, tightly-controlled use of side-effects, and very powerful type system) and deficient in others (five string types).  Python achieves good regimentation despite its lack of types, which I believe is a crucial factor in its popularity.

Making Complex Ideas Accessible

A key to success in industrial development is the ability to make a complex idea accessible.  In my own experience, this was one of the core design principles of the Lambda project in Java.  We had the challenge of introducing higher-order functional programming and all the notions that come along with it in a way that was accessible to programmers used to the stateful OO style of thinking.  Conversely, many efforts have gotten this wrong, as exemplified in the infamous quote “a monad is just a monoid in the category of endofunctors”.

This translation between idioms is quite difficult; it requires one to deeply understand both sides of the fence, as well as which use cases and concerns are most common on both sides.  However, it’s critical- people don’t use what they can’t understand.  The best way to facilitate understanding is to present an idea or principle in a context the audience already understands.


Just as failure must be dealt with in the context of software systems, changing behavior and practices must be dealt with in the context of human factors.  As an example, programming practices based on the functional paradigm are becoming increasingly recommended practice due to a number of changing factors in the world.  Many languages face the challenge of adapting their user base to these new practices.

The mentality of harm-reduction often proves the most effective attitude when it comes to changing human behavior, both here and elsewhere.  Harm-reduction accepts that “bad” behavior takes place and focuses its efforts on minimizing the negative impacts on oneself and others and encouraging a transition towards better behavior in the long-run.  This reflects the realities of industrial programming: software can’t be rewritten into a new paradigm all at once, and some legacy systems can’t be eliminated or rewritten at all.

In the design of industrial languages and tools, this takes the form of several adages I’ll list here: provide options instead of demands, minimize upfront costs and facilitate gradual transitions, work with the old but encourage the new.

On Seeming Contradictions

It might seem, particularly to the more academically and philosophically inclined, that many of these principles I’ve elaborated contradict each other.  How can we provide regimentation while working with the mentality of harm-reduction?  How can we restrict use to the “good” behaviors while gracefully handling failure?

The solution is in itself another critically important principle: the notion of avoiding absolutist conflicts of ideas.  In the practical world, ideas tend to be useful in certain contexts, and a given principle needs to be evaluated in the context of use.  Put another way, “it’s important to use the right tools for the job”.

On a deeper level, ideological wars tend to end with both sides being “wrong”, and often some synthesis of the two being right.  In physics, the debate over whether light was a wave or a particle raged for centuries; in truth, it’s both.  There are many other such examples throughout history.


If we reduce everything I’ve discussed down to its essence, we arrive at the following statement: as the scale of industrial programming increases, the dominant concerns become irreducible complexity and inelegance, and human factors associated with coordinating effort.  Thus, “industrial pragmatics” refers to a set of techniques and principles for managing these concerns, and industrial programming languages are those languages that consider these techniques in their design.


Slides and Notes from Last Year’s Denotational Semantics Introduction

Last year, I gave a talk at Boston Haskell introducing people to the basics of denotational semantics, starting with Scott’s domain theory and touching on the metric space approaches as well.  I never did post the slides or notes from that talk.

The slides can be found here, and the notes here.

Slides from Making Category Theory Accessible Talk

I have been working on ideas for how to make category theory more accessible and easier to learn, with the belief that it could be eventually be reorganized to the point where it could be taught to high school students interested in math.

I gave a 20-minute talk yesterday at Boston Haskell about the progress of my ideas so far.  This stimulated some interesting discussions.  I am posting the slides here.

Cohabiting FreeBSD and Gentoo Linux on a Common ZFS Volume

My Librem 15 arrived a while back.  I normally prefer FreeBSD for just about everything, but I need access to a Linux OS running on the Librem platform in order to help me port over some remaining device drivers (namely the BYD mouse and screen brightness).

In order to facilitate this, I’ve installed a setup I developed a while back: that of a dual-booted FreeBSD and Gentoo Linux system living on the same ZFS volume.  This article details how to achieve this setup.

Note that this article is based on the EFI bootloader.  If you insist on legacy BIOS boots, you’ll need to adapt the procedure.

Overview of the Scheme

The scheme is based on a somewhat atypical use of the ZFS filesystem (namely foregoing the mountpoint functionality for the OS datasets in favor of an fstab-based approach) combined with GRUB to achieve a dual-bootable OS

ZFS Overview

The ZFS system differs slightly from the “typical” ZFS setup on both FreeBSD and Linux.  Some datasets (namely the home directories) are shared between both operating systems, but the OS datasets differ in their mount-points depending on which OS we are using, and thus the ZFS-specific mountpoint functionality can’t be effectively used.

In this article, assume that the volume’s name is “data”.

The overall scheme looks something like this:

  • data/home is mounted to /home, with all of its child datasets using the ZFS mountpoint system
  • data/freebsd and its child datasets house the FreeBSD system, and all have their mountpoints set to legacy
  • data/gentoo and its child datasets house the Gentoo system, and have their mountpoints set to legacy as well

OS and GRUB Overview

Both OSes must utilize the /etc/fstab method for mounting most of their filesystems, since we cannot make use of the ZFS mountpoint functionality.  This requires a different fstab for each OS.  Note that the data/home dataset (as well as any other similar dataset) will be mounted using the ZFS mountpoint method, not fstab.

Additionally, both OSes have access to the other OS’ data through a special top-level directory (/freebsd on Gentoo, /gentoo on FreeBSD).

The GRUB bootloader can be used to provide a workable boot selection facility without any serious modification or configuration (other than knowing the magic words to type into the grub.cfg file!)

Setup Procedure

The setup procedure consists of the following steps:

  1. Use the FreeBSD installer to create the GPT and ZFS pool
  2. Install and configure FreeBSD, with the native FreeBSD boot loader
  3. Boot into FreeBSD, create the Gentoo Linux datasets, install GRUB
  4. Boot into the Gentoo Linux installer, install Gentoo
  5. Boot into Gentoo, finish any configuration tasks

Note that nothing stops you from reversing the procedure, installing Gentoo first, and using its tools.  I just find that GPT creation and GRUB installation go a lot more smoothly on FreeBSD.

Getting Ready

To perform the setup procedure, you’ll need installer memstick images for both OSes.  FreeBSD’s installer can be gotten here; Gentoo’s can be gotten here (use the livedvd ISO).  You’ll also need some means of internet access (of course).

Note that in the case of the Librem 15 or similar laptops which have no ethernet connector, you may need to adopt a slightly modified procedure of installing Gentoo’s wireless tools and wpa_supplicant during the main installation.

FreeBSD Installer

Boot into the FreeBSD installer, go through the boot menu, and select manual partitioning mode.  This will drop you into a shell and ask you to create your partitions and mount everything at /mnt.

Create Partitions and ZFS Pool

The first thing to do is use the gpart tool to create your partitions.  FreeBSD’s man pages are rather good, so you can use “man gpart” to get the guide to the tool.  My procedure on the Librem 15 looks like this:

gpart create -s gpt ada0
gpart create -s gpt ada1
gpart add -t efi -l efi-system -s 200M ada0
gpart add -t freebsd-zfs -l zfs-data ada0
gpart add -t linux-swap -l swap -s 96G ada0
gpart add -t freebsd-zfs -l zfs-data-log -s 16G ada0
gpart add -t freebsd-zfs -l zfs-data-cache ada0

Then create a ZFS pool with the new partitions, and format the EFI system partition with the DOS filesystem (seriously, why do we still use that thing?):

newfs_msdos /dev/ada0p1
zpool create -m legacy -o atime=off -o checksum=sha256 data /dev/ada0p2 log /dev/ada0p2 cache /dev/ada0p3

Note that we’ve turned off atime (which reduces disk write traffic considerably) and set the checksum algorithm to sha256.

The ada1 disk is a SSD I had installed.  If you don’t have an SSD, it doesn’t make any sense to have a log or a cache.  The 16GB intent log is way overkill, but it reduces the strain on the device.  Note that we set the root dataset’s mountpoint to “legacy”.

Note that linux has its own swap format, so we can’t share the swap device.

Create the ZFS Datasets

Now that you have a ZFS pool, the first thing you’ll need to do is create the datasets.   Start by creating the FreeBSD root and mounting it (note that it will inherit the “legacy” mountpoint from its parent):

zfs create -o compression=lz4 data/freebsd
mount -t zfs data/freebsd /mnt/

We need to create some mountpoint directories:

mkdir /mnt/home
mkdir /mnt/gentoo/
mkdir /mnt/tmp
mkdir /mnt/usr
mkdir /mnt/var

I use a fairly elaborate ZFS scheme, which applies different executable, setuid, and compression properties for certain directories.  This achieves a significant compression ratio, effectively increasing the size of my disks:

zfs create -o exec=on -o setuid=off -o compression=off data/freebsd/tmp
zfs create -o exec=on -o setuid=on -o compression=lz4 data/freebsd/usr
zfs create -o exec=off -o setuid=off -o compression=gzip data/freebsd/usr/include
zfs create -o exec=on -o setuid=off -o compression=lz4 data/freebsd/usr/lib
zfs create -o exec=on -o setuid=off -o compression=lz4 data/freebsd/usr/lib32
zfs create -o exec=on -o setuid=off -o compression=gzip data/freebsd/usr/libdata
zfs create -o exec=on -o setuid=on -o compression=lz4 data/freebsd/usr/local
zfs create -o exec=on -o setuid=off -o compression=gzip data/freebsd/usr/local/etc
zfs create -o exec=off -o setuid=off -o compression=gzip data/freebsd/usr/local/include
zfs create -o exec=on -o setuid=off -o compression=lz4 data/freebsd/usr/local/lib
zfs create -o exec=on -o setuid=off -o compression=lz4 data/freebsd/usr/local/lib32
zfs create -o exec=on -o setuid=off -o compression=gzip data=freebsd/usr/local/libdata
zfs create -o exec=on -o setuid=off -o compression=gzip data/freebsd/usr/local/share
zfs create -o exec=off -o setuid=off -o compression=off data/freebsd/usr/local/share/info
zfs create -o exec=off -o setuid=off -o compression=off data/freebsd/usr/local/share/man
zfs create -o exec=on setuid=on -o compression=lz4 data/freebsd/obj
zfs create -o exec=on -o setuid=on -o compression=lz4 data/freebsd/usr/ports
zfs create -o exec=off -o setuid=off -o compression=lz4 data/freebsd/usr/ports
zfs create -o exec=on -o setuid=off -o compression=gzip data/freebsd/usr/share
zfs create -o exec=off -o setuid=off -o compression=off data/freebsd/usr/share/info
zfs create -o exec=off -o setuid=off -o compression=off data/freebsd/usr/share/man
zfs create -o exec=off -o setuid=off -o compression=gzip data/freebsd/usr/src
zfs create -o exec=off -o setuid=off -o compression=lz4 data/freebsd/var
zfs create -o exec=off -o setuid=off -o compression=off data/freebsd/var/db
zfs create -o exec=off -o setuid=off -o compression=lz4 data/freebsd/var/db/pkg
zfs create -o exec=off -o setuid=off -o compression=gzip data/freebsd/var/log
zfs create -o exec=off -o setuid=off -o compression=off data/freebsd/var/empty
zfs create -o exec=off -o setuid=off -o compression=gzip data/freebsd/var/mail
zfs create -o exec=on -o setuid=off -o compression=off data/freebsd/var/tmp

Because FreeBSD is pretty strict about where certain files go, this scheme works pretty well.  You could of course continue to subdivide it up to your heart’s desire, creating more subdirectories in /usr/share and such.

For Gentoo, you’ll probably want a simpler scheme, as Linux tends to be much sloppier about the locations of things:

zfs create -o exec=on -o setuid=off -o compression=off data/gentoo/tmp
zfs create -o exec=on -o setuid=on -o compression=lz4 data/gentoo/usr
zfs create -o exec=off -o setuid=off -o compression=lz4 data/gentoo/var

A Gentoo master might be able to subdivide this up as I’ve done with FreeBSD.

The final task is to mount all these filesystems manually with the following command template:

mount -t zfs data/freebsd/<path> /mnt/<path>

This is necessary, as all the mount-points will be “legacy”.  I won’t waste space by showing all the commands here.

Install and Configure the FreeBSD system

Now type “exit”, which will drop you back into the FreeBSD installer, with everything mounted at /mnt/.  The remainder of the installation procedure is straightforward.  However, you’ll need to opt to go to a shell for two final configuration tasks.

Go to the shell, then enter into the new FreeBSD system

chroot /mnt

Create the fstab

Since we mount the vast majority of the ZFS datasets to different paths in each OS, we’ll need to create an /etc/fstab file for them.  The following fstab will mount all the datasets to the right locations:

data/freebsd/tmp /tmp zfs rw 0 0
data/freebsd/usr /usr zfs rw 0 0
data/freebsd/usr/include /usr/include zfs rw 0 0
data/gentoo/ /gentoo zfs rw 0 0
data/gentoo/tmp /gentoo/tmp zfs rw 0 0
proc /proc procfs rw 0 0

Note that I’ve left out all a number of the entries.  You’ll have to map each dataset to its proper path as shown above.

Install the FreeBSD Native Bootloader

We’ll need the FreeBSD bootloader to get into the system for the first time.  Install it to the with the following procedure:

mount -t msdosfs /dev/ada0p1 /mnt
mkdir /mnt/efi
mkdir /mnt/efi/BOOT
cp /boot/boot1.efi /mnt/efi/BOOT/BOOTX64.EFI

The last thing you’ll need to do is set the bootfs parameter on the zpool, so the FreeBSD bootloader will pick the right dataset:

zpool set -o bootfs=data/freebsd data

You may also need to set the bootme flag on the EFI system partition for some hardware:

gpart set -a bootme -i 1 ada0

Your system is now ready to boot into the OS directly.

FreeBSD Main OS

You should now be able to boot into FreeBSD directly.  You’ll need to connect to a network, which may involve wpa_supplicant configuration.

Before doing anything else, I usually pull down the latest sources and rebuild world and the kernel first.  This ensures my system is up-to-date.  There are plenty of guides on doing this, so I won’t waste the space describing how to do it here.

You’ll also need to obtain the ports collection.  Again, there are plenty of guides on doing this.

Installing GRUB

The grub-efi port will install a version of GRUB capable of booting an EFI system.  This port is much easier to use in my opinion than the Gentoo equivalent.  The port is installed as follows:

cd /usr/ports/sysutils/grub2-efi
make install clean

At this point, you’ll need to create a grub.cfg file.  The grub-mkconfig command gets a good start, but you’ll inevitably need to edit it.  You can also just use the following file directly (make sure it’s at /boot/grub/grub.cfg):

insmod part_gpt
insmod zfs

menuentry 'FreeBSD' --class freebsd --class bsd --class os {
  search.fs_label data ZFS_PART
  echo "Loading FreeBSD Kernel..."
  kfreebsd ($ZFS_PART)/freebsd/@/boot/kernel/kernel
  kfreebsd_loadenv ($ZFS_PART)/freebsd/@/boot/device.hints
  kfreebsd_module_elf ($ZFS_PART)/freebsd/@/boot/kernel/opensolaris.ko
  kfreebsd_module_elf ($ZFS_PART)/freebsd/@/boot/kernel/acl_nfs4.ko
  kfreebsd_module_elf ($ZFS_PART)/freebsd/@/boot/kernel/zfs.ko
  set kFreeBSD.vfs.root.mountfrom=zfs:data/freebsd
  set kFreeBSD.vfs.root.mountfrom.options=rw

menuentry 'Gentoo Linux' {
  search.fs_label data ZFS_PART
  linux ($ZFS_PART)/gentoo@/boot/kernel dozfs=force root=ZFS=data/gentoo
  initrd ($ZFS_PART)/gentoo@/boot/initramfs

Note that we’ve created an entry for Gentoo, though it doesn’t yet exist.  Last, you’ll need to mount your EFI system partition and install GRUB:

mount -t msdosfs /dev/ada0p1 /mnt
grub-install --efi-directory=/mnt --disk-module=efi

This will install the GRUB boot program to /efi/grub/grub.efi on the EFI system partition.  You’ll need to copy it into place.  However, I recommend making a backup of your FreeBSD native bootloader first!

cp /mnt/efi/BOOT/BOOTX64.EFI /mnt/efi/BOOT/BOOTX64.BAK

This will simplify the recovery for you if things go wrong.  Now, copy the GRUB boot loader into place:

cp /mnt/efi/grub/grub.efi /mnt/efi/BOOT/BOOTX64.EFI

You should test your GRUB bootloader once to make sure it works by rebooting the system and booting into FreeBSD.  Don’t try to boot into Gentoo yet, as nothing is there!

Gentoo Installer

Your next task is to install the Gentoo base system.  Gentoo installation is done manually via the command line.  A guide is provided by the Gentoo Handbook.  Note that because you’re using ZFS as a root filesystem, you’ll need to do things a bit differently, and you will have to use genkernel to install your kernel!

Mount the Filesystems

As with FreeBSD, you’ll need to mount the filesystems:

zpool import -f data
mount -t zfs data/gentoo /mnt/gentoo
mkdir /mnt/gentoo/tmp
mkdir /mnt/gentoo/usr
mkdir /mnt/gentoo/var
mount -t zfs data/gentoo/tmp /mnt/gentoo/tmp
mount -t zfs data/gentoo/usr /mnt/gentoo/usr
mount -t zfs data/gentoo/var /mnt/gentoo/var

Now follow the Gentoo install steps and everything should go smoothly.

Creating the fstab

As with the FreeBSD system, you’ll need to create an /etc/fstab file.  The file looks similar to the FreeBSD version, but with the gentoo filesystems mounted relative to root and the FreeBSD filesystems mounted relative to /freebsd:

data/freebsd/tmp /freebsd/tmp zfs rw 0 0
data/freebsd/usr /freebsd/usr zfs rw 0 0
data/freebsd/usr/include /freebsd/usr/include zfs rw 0 0
data/gentoo/tmp /tmp zfs rw 0 0
data/gentoo/usr /usr zfs rw 0 0

Again, I’ve left out the repetitive portions of the file.

Building the Kernel, ZFS Modules, and initramfs

As we are booting from a root ZFS filesystem, you’ll need to set up a kernel with ZFS support.  You can find a guide to doing this here (skip down to the “Configuring the Kernel” section and go from there).

Note that I’ve set up the GRUB installation to go after /boot/kernel and /boot/initramfs.  Gentoo by default installs its kernel to /boot/kernel-<version information>, and the same with initramfs.  You’ll need to create symlinks with the name /boot/kernel and /boot/initramfs, or else copy the files into the right place yourself.

Final Gentoo Installation

Before you reboot, you’ll need to make sure that you’re read.  Here is a checklist of things I forgot and had to reboot into the installer to do:

  • Set a root password so you can actually log in
  • Install the ports to use wireless
  • Don’t miss a volume in /etc/fstab (if you miss /var, portage will get very confused)

Boot into Gentoo

You should now be able to boot into Gentoo directly from GRUB.  Congratulations!  You now have a dual-boot, single-ZFS system!  The last thing you’ll want to do before you create an user home directories is create a ZFS dataset for /home.  In the Gentoo system, do the following:

rm /home || rmdir /home
rm /freebsd/home || rmdir /freebsd/home
mkdir /home
mkdir /freebsd/home
zfs create -o mountpoint=/home -o exec=on -o setuid=off -o compression=lz4 data/home

You may also want to create datasets for specific users’ home directories (or even subdirectories thereof).  Note that we’ve set the mountpoint to /home.  This will cause the ZFS mountpoint functionality to mount those datasets, so there’s no need to add an fstab entry.


I have found this setup to be quite powerful and flexible, especially for kernel hackers and driver developers.  The following are some of the benefits of the setup:

  • Ready access to a full Linux system, including kernel sources from the FreeBSD system.
  • Convenient switching between systems for experimentation purposes
  • Effective recovery mechanism if one system gets broken

There’s also some interesting room for work with the FreeBSD Linux emulation layer here.  Normally, the FreeBSD Linux emulation ports install a minimal set of Linux packages.  I don’t know the subsystem well enough to do it myself, but I imagine there’s serious potential in having a full Linux installation at your disposal.

Slides from My IEEE SecDev Talk

I gave a talk at IEEE SecDev on Nov 3 about my vision for how to combine industrial programming language pragmatics with formal methods.  The slides can be found here.

This was a 5-minute talk, but I will be expanding it into a 30-minute talk with more content.