[tlug] A First Hello

[eizietheez@example.com]

Hello TLUG,

This is my first message here, though I have a smattering of nomikai. Name is
Brandon Wilson; I am a friend of Joe Larabell's. Hopefully, that rings a few
bells.

I have tried subscribing a few times in the past without success---the
subscription request emails falling into a black hole. Between my first
attempts and now, I got the PTR DNS record correctly setup for my domain, so my
guess is that spam filtering was the culprit.

Anyway, for the past year I have been banging my head against the job market,
trying to find a position in a remote work position. A fellow TLUG member
suggested that posting here might be helpful. That's what prompted me to try
again. I hope this kind of post isn't breaching the list ethos.

Below is a link to my CV, but since this is my first post, I figure a bit of an
introduction is appropriate.


My first introduction to Linux was in middle school. For unknown reasons, me
and my friends at the time were sort of wannabe Linux fanboys for several
years, until I got my first hand-me-down laptop with which I immediately
installed Mandrake Linux and leveled up into a proper Linux fanboy.

In the intervening years I have pretty much used Linux exclusively. My high
school years were dominated by Gentoo, but in college I was gifted what is
probably the most interesting personal machine I have ever owned---one of those
OLPC machines with a hand crank for emergency power.

Later, I ended up running Arch for several years, and these days I am running
Void Linux, a non-systemd, libressl, minimalist distro using its own package
manager xbps. I like it well enough, but the reproducibility bug has bit me
hard and now I am slowly migrating over to Guix.

I recently bought a Thinkpad T400s---the same machine Stallman uses---and am
working to acquire the hardware necessary to flash libreboot over the bios.
This I plan to turn into a Xen machine running Guix as its dom0, as as sort of
DIY Qubes OS.

Anyway, apart from that, I also managed to get a full Guix System running on
Google Cloud Compute and am in the process of of migrating my current
wilsonb.com host machine over to this.

Some random projects I am working on and would love some nerd-out buddies on
include

* Hand-written ELF files (git://git.wilsonb.com/hello-world.git),

In an attempt to get a concrete understanding of exactly how a process
executes, I started with the executable file itself. So far I have a simple
statically-linked hello world elf file written directly as .byte instructions
in GNU assembler. The work in progress is turning this into a
dynamically-linked executable, but I'm having issues getting ld.so to perform
relocations.

* Random projects in J (git://git.wilsonb.com/j-play.git), and

The J and APL programming languages I find fascinating. They are like
executable math notation. Currently, I am just going through Project Euler
problems and coding them as pure tacit J verbs. However, a future project idea
I have is a J compiler in J. The inspiration comes from Aaron Hsu's co-dfns
compiler for Dyalog APL.

* Playing with formal proof verification (http://us.metamath.org/)

My academic background is in math, and one of the coolest recent discoveries I
have made is the formal verification system Metamath. Playing with formal
verified proofs sort of marries the tinkerability of software with the stark
beauty of rigorous math proofs. Other systems like Coq, Lean, and Mazar are
really powerful, but the verification software itself is really complex and
*hard codes* the foundations into the verifiers. Metamath, however, is this
really tiny language that defines a meta-language for *any* formal logical
system.

There is a community database of proofs, https://github.com/metamath/set.mm,
that implements ZFC and a whole bunch of standard mathematics---the proof that
Fourier transforms work, geometry, etc. But there are other databases (with
less active contributors) that do math from different foundations. Also, the
Metamath language itself is small enough there are *several* verifier
implementations, all of which give a thumbs up to the various public databases.

Some other topics I find highly intriguing:

* GNU/Hurd,
* Plan 9,
* Haskell,
* x86 bootstrapping (and early Coreboot), and
* Fuzzing the x86 instruction set (https://invidio.us/watch?v=KrksBdWcZgQ).


Anyway, I am glad to finally be on the list here, and hope to nerd out with you
all!

Cheers,
Brandon Wilson


P.S.

As promised, here is my CV:

    https://wilsonb.com/cv.pdf

Please help me connect with someone who could use my skills and enthusiasm!