Better infrastructure through types

  • Composable Sequenced Processes

    This blog series demonstrates how typed functional programming is relevant in operations and why you should care using simple, yet practical and motivating examples. This post will walk through writing automation for secrets management: we will verify a signature of an encrypted document, decrypt the document, verify a signature for the decrypted document.

  • Algebraic Data Types

    NOTE: This is an edit of an article I wrote for Functional Algebra in 2012.

  • The Unreasonable Effectiveness of Reasoning: Eliminating Bottom

    This article provides a simple code-level case study to understand how two functional programming libraries have made different trade-offs. We explore related API-level design choices in a neutral language (Scala) where we consider the ability of the consumer of the API to reason equationally about it. We demonstrate that focusing on eliminating bottom yields more reasonable (equationally) APIs.

  • Extending Syntax in Scala

    Yesterday I learned something really cool. In Idris I can just do this to extend the syntax:

  • Why Use Types?

    Types are one of the most mainstream and widespread applied formal methods in software engineering industry today. Yet I have met many accomplished and experienced practitioners in our field who do not know how to effectively use types, even in lanuages they can leverage well for this.