About Me
My name is Nathan, I'm an engineering psychologist by training, and a systems engineer by trade.
I've had the good fortune to work professionally with rust for some time, as well as some other oddball languages like Haskell and F# back in the day. I current work for a state university's disability support center doing pretty mundane, but worthwhile webdev work.
I've previously worked in, and greatly enjoy working with, distributed systems. I also have deep interests in cryptography, authenticated data structures, archival, and formal verification methods.
Much of my recent hobby programming has revolved around a neat little language called Idris2, which is notable for revolving around dependent types while still being programmer focused rather than theorem proving focused. Dependent Typing has a lot of potential benefits for normal every day programmers, from being able to more easily express constraints in the type system to more easily getting the type system out of the way when you need to without losing its benefits, and you can expect to see a lot of programmer oriented content on dependent types on this blog.
My Projects
Rust
I don't do hobby work in rust very much anymore, but I've been around the ecosystem and still kick around in some rust spaces.
You may remember me from my work on Asuran, which has been on indefinite hiatus for a while now. Rust's type system's relative lack of power, particularly in the area of preventing common cryptography bugs without becoming overly verbose or relying on the library programmer to pinky promise to uphold their own invariants was a big motivator for me moving away from rust, and I hope to eventually pick Asuran back up some day and rewrite it in Idris or some other fun new language.
Idris 2
I've written a few libraries and utilities for Idris 2 already:
-
A sized rope data structure for text manipulation
-
A collection of implementations of useful data structures
-
A collection of prototype tools for working with Idris projects. Currently provides comment-based unit testing capability. Currently written in Raku, I hope to eventually rewrite this in idris.
Raku
-
The static site generator powering this blog. This is a horribly cursed tangle of ill-thought-through raku code that is not meant to be reused. Feel free to take a look and maybe take inspiration from it, or at the very least feel better about your own just-get-it-done code, but don't let me catch you forking it.
Books
Idris by Highly Contrived Example
A very work in progress project to explore functional programming and dependent typing concepts by solving every advent of code problem in one big literate Idris project, only taking small steps in understanding with each new day.