I wanted to make a vs-code extension that others might not simply rewrite or dismiss when seeing the inside of it not written in a mainstream language, so I was looking for a good elm-like framework. React is close to this but still tragically broken on state, so I wanted…


Sometimes you have disjoint but covering class instances for a type in idris. …


why things are kind of awful and perhaps a way toward away from awfulness

tldr; Often, we’re working to a deadline that should be a “delivery timebox”, and our narrow focus on “outcomes” often blinds us to the ways we can get more smarter without breaking everything.

My theses:

  • We…


I wanted alists with guaranteed unique values, and finally decided to sit down and work out how this functions in idris. For those not as old as dirt, an alist in lisp is a list of pairs where the (car) of each is considered to be the key, so it…


Two things I learned from this:

  1. If you write objects with values encoded at both runtime and compile time, you can use type classes to guide Idris through induction on them rather than having to reimplement it as proof code. Not only that, but the compiler can act as a…

A perennial source of angst for me is dealing with plans and deadlines in software. While there are many takes on this from #NoEstimates to good old blame, it’s a common experience that neither the people making the estimates, nor those receiving them are making any use of the information…


Hot take: https://twitter.com/deech/ has made https://github.com/deech/libclang-static-build ← a simple static build of libclang that allows you to bust your libtooling and other clang related code out of llvm build tree jail and api version hell.

One of my previous lives involved writing a lot of C++ and I became very…


I’ve been deep diving idris for a while, and the way certain dependently typed structures change type over time has been something I haven’t had a great handle on. …


I had something on my mind earlier and admittedly i wasted precisely 37 minutes just now advancing a proof target I’m working on.

I’d had trouble with proofs like “a < b implies f a b = []” for some a and b. The problem comes when you case split…


Recently, in order to give a coworker an easier way to interact with some code we deliver as javascript, I ported something from bucklescript to fable so that it’d be visible in a .net IDE. Admittedly, the result is pretty swank. …

art yerkes

An old programmer learning new tricks.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store