I am from Christchurch, New Zealand.

At the moment, I am studying law at the University of Canterbury in Christchurch, New Zealand.

BSc(Hons) in Mathematics with First Class Honours

BSc in Mathematics and Computer Science

I have two and a half years of work experience as a software developer at two New Zealand software development companies.

I have tutored a number of mathematics and computer science courses at the University of Canterbury in Christchurch, New Zealand, including MATH102/MATH103 (first year calculus and linear algebra), MATH120 (discrete mathematics), MATH220 (graph theory and cryptography), MATH230 (logic, automata and computability), COSC121 (introductory programming) and COSC367 (artificial intelligence).

- Æther is an implementation of a chat protocol of my own design, which is named Ætherwind. It is
intended to be a federated end-to-end-encrypted chat protocol with support for both private and public permanent channels (think
optionally-end-to-end-encrypted IRC) and for 1-to-1 and small group ephemeral chats (think Signal).
A blog post by Drew DeVault, the creator of sway and Sourcehut, was
the main inspiration for Æther(wind).
Æther is implemented using the Monocypher library which provides cryptographic primitives. It is a reference implementation, intended to demonstrate the potential of the protocol and not to be all things to all men. The protocol itself uses standard modern cryptography (Curve25519, ChaCha20, Poly1305, BLAKE2, HKDF, Argon2) and should be easy to implement using any library of modern cryptographic primitives.

- QED is a proof assistant and programming language for constructive Morse set theory written in Haskell. It is currently on hold.
- Minimal logic is a proof checker for minimal propositional logic written in Haskell. I wrote this project as part of my BSc(Hons) in Mathematics. It uses the Haskell type system to prevent the representation of structurally invalid proofs. It also includes a minimal propositional Kripke model checker also written in Haskell. It is no longer under development.
- Visp is a simple Lisp written in Python, with macros, using substitution to evaluate (not metacircular, but does use the Python stack). As an experiment, Visp is complete. I hope one day to find the time to revisit Visp and fexprs.
- Sceptre is a fun little automatic theorem prover for minimal propositional logic written in Racket.
- my
`vim`configuration—be sure to use`--recurse-submodules`to clone this.

Please contact me at miles@rout.nz.