66 lines
2.7 KiB
Markdown
66 lines
2.7 KiB
Markdown
|
# 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](https://github.com/idris-lang/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](https://sr.ht/~thatonelutenist/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:
|
||
|
|
|
||
|
|
- [rope](https://git.sr.ht/~thatonelutenist/idris2-rope)
|
||
|
|
|
||
|
|
A sized rope data structure for text manipulation
|
||
|
|
|
||
|
|
- [Structures](https://git.sr.ht/~thatonelutenist/Structures)
|
||
|
|
|
||
|
|
A collection of implementations of useful data structures
|
||
|
|
|
||
|
|
- [iutils](https://git.stranger.systems/Idris/iutils-raku)
|
||
|
|
|
||
|
|
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.
|
||
|
|
|
||
|
|
### Books
|
||
|
|
|
||
|
|
- [Idris by Highly Contrived Example](https://static.stranger.systems/idris-by-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.
|