Haskell at Galois

Galois Inc. is an employee-owned software development and computer science research company based in Portland, Oregon, U.S.A. Galois began life in late 1999 with the stated purpose of using functional languages to solve industrial problems.

Galois develops software under contract, and many of our projects use Haskell. We’ve delivered tools, written in Haskell, to clients in industry and the U.S. government. Here are some diverse examples:

  • Cryptol, a domain-specific language for cryptography (with an interpreter and a compiler)
  • HaLVM, a port of the GHC runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen’s “bare metal”
  • SMACCMPilot, an embedded systems software research project where we are building open-source autopilot software for small unmanned aerial vehicles (UAVs) using new high-assurance software methods.

We’ve also done work on homomorphic encryption (computation on encrypted data), design and analysis of trust-worthy virtualization platforms (think the infra-structure behind cloud-based web services), analysis and specification of policies (matching machine-checkable policies with natural language specs), tools for software development and analysis (e.g., static analyzers, compilers, interpreters, debuggers, etc.)

Haskell use

So, why do we use Haskell? There are benefits to moving to Java or C# from C++ or C, such as cleaner type systems, cleaner semantics, and better memory management support. But languages like Haskell give you a lot more besides: they’re much higher level, so you get more productivity, you can express more complex algorithms, you can program and debug at the “design” level, and you get a lot more help from the type system. These arguments have been made time and again though, and they’re also pretty subjective.

For Galois, it’s also a big bonus that Haskell is close to its mathematical roots, because our clients care about “high assurance” software. High assurance software development is about giving solid (formal or semi-formal) evidence that your product does what it should do. The more functionality provided, the more difficult this gets. The standard approach has been to cut out functionality to make high assurance development possible. But our clients want high assurance tools and products with very complex functionality. Without Haskell (or some similar language, like ML or OCaml), we wouldn’t even be able to attempt to build such tools and products.

At Galois, we’re happily able to solve real world problems for real clients without having to give up on using the tools and languages we worked on when we were in the Academic world. In fact, we credit most of our success with the fact that we can apply language design and semantics techniques to our clients’ problems. Functional languages are an integral part of that approach, and a big part of the unique value that our clients have come to know us for.

The good news is that this has worked quite well. Galois has three offices (Portland, OR, Dayton, OH, and Arlington, VA) and about 100 employees as of Summer, 2019. We have experienced solid growth, and our clients include most branches of the U.S. Department of Defense, the Intelligence Community, NASA, Amazon, and Microsoft.

We are also quite involved in the functional programming community: we sponsor numerous conferences (e.g., ICFP, PLDI), we participate in the Haskell.org committee and various Haskell standardization efforts, and we contribute code towards the Haskell eco-system: both by writing new open source tools and libraries, and by improving and extending existing ones.

For more information, see https://galois.com/research-development/