Exploring Dependent Types in Idris

Dependent Types

When I’m not coding the "impossible" at Art+Logic, I take a lot of interest in new programming technologies and paradigms; even if they’re not yet viable for use in production, there can often be takeaways for improving your everyday code.

My current fascination is the Idris programming language, a research language built around making dependent types practical. This is a quick primer on what dependent types are, how they work in Idris, and how they can change the way you think about types in other languages; we’ll assume no prior knowledge of Idris or of purely functional languages in general, but a basic familiarity with functional programming will make things easier to follow.


Legacy Vulnerabilities AKA Software Senescence

software senescence

Does your business still have an XT computer in the back office because it’s running that one version of some database software that your business depends on? Yeah, we know there is. Most modern software doesn’t work like that.

If you aren’t keeping your custom software up with the changing computing environment, it will fail not necessarily because it has flaws, or the hardware can no longer meet the demand, but because the support your software relies upon has changed.

Let’s look at the vulnerabilities you must manage so that your software does not reach its end of life before losing its inherent usefulness.


Asynchronous Python – A Real World Example

Complex Conversions


We have a customer that developed a hardware device to make physical measurements. Some years ago we wrote a suite of software tools for the customer: a tablet application for configuring the hardware device, a django web server to receive uploaded XML documents generated by the device, and a user-facing web application (using the same django server), providing reporting and data analytics.


Smooth Upgrades to Vue 3 Using the Migration Build

2 v 3 — Vue updgrade graphic

Vue 3 introduces some compelling new features, but also many breaking changes. The question is, how do you get there? Fortunately, the Vue.js team has recently released the Migration Build, which makes it possible (and easy) to make a smooth transition from v2 to v3.


What we’re reading now and were reading at the end of 2020 . . .

What we're reading January 2021 edition

Well, normally we like to share this list just around the holidays. 2020 being what it was, I suppose it’s not surprising that this list should show up as we get closer to the end of January 2021 than the end of last December. Anyway, here’s a list of some of the stuff we were reading at the end of last year and might still be reading now.


Here’s an Idea for an App: “Shopping Friends”

Illustration for shopping friends app idea

"Shopping Friends" is a service that analyzes your Amazon buying patterns and matches you with like-minded people.

Maybe it’s a Facebook app. When you join, you give it permission to access your Amazon shopping records, and maybe there are some filters for what kind of people you want to be matched with (e.g. same country versus anywhere in the world). There would need to be a preferences control panel that you can get to somehow to change these filters afterward.


Creativity in Software Testing

Software testing illustration

What’s in a name? Well, in the case of Art+Logic, our name conveys the idea that software development is a combination of both art and logic. We find this to be the case in all aspects of the software development life cycle. And this is definitely true with software testing.


Bringing an Idea to Life: WatchWah Proof of Concept

Image of Guitar and Apple Watch

"Wouldn’t it be cool if…"

We’ve all had that thought about something. How do you get from there to a product you can use and share with others? When I found myself playing with an idea that seemed exciting and new, I decided to capture some notes on the process, from the perspective of an Engineering Manager at a company that’s all about implementing people’s creative visions.