Typed holes are an amazing tool in a developer’s toolbox. The holes give hints via types how to finish an implementation. They’re available in Haskell, Agda and Idris.
Category Archives: ephemera
The State of Software Engineering
Aside
The state of software engineering is best illustrated by an XKCD on voting software.
Haskell IDE Engine in the Atom Editor from cwd
Aside
To get the Haskell IDE Engine working in the Atom editor, one has to start Atom in the directory of a project. I’d call this a bug.
Idris 1.3.0 Released
Aside
It happened two months ago, but Idris 1.3.0 is out.
Incomplete Pattern-matching in Haskell
Aside
From Haskell’s safe-exceptions library: “[I]ncomplete pattern matches can generate impure exceptions.” This makes me think of Agda, its totality and absence of exceptions.
2FA Smartphone App
Status

Whenever they tell you that you have to install a very specific proprietary software smartphone app for two-factor authentication such as Google Authenticator or Authy, just nod, install a free software app such as andOTP and pretend you’re following instructions. It will work without them noticing you use free software.
Haskell User Survey 2018
Status

If you’re interested in how Haskell adoption in practice looks like in 2018 compared to 2015, read the State of Haskell 2018 user survey’s results by FP Complete.
Felleisen on Dynamically Typed Languages
Status

“If you are not married, if you don’t want to spend time with your kids, if you hate vacations, [dynamically typed languages] is the way you program!” ~ Matthias Felleisen
On Dynamically Typed Languages
Status

“Test-driven development replaces a type checker in a dynamically typed language in the same way that a bottle of whiskey replaces your daily problems.” ~ Matt Gumbley
Debian Meltdown
Status

For some reason it happened only a few days ago that Debian GNU/Linux in the current stable release code-named Stretch got a kernel patch for the meltdown horror. That’s over two full months since Meltdown made it to news.