Miles Rout

Links

• milesrout on GitHub
• milesrout on SourceHut

Projects

• Æ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.

Contact Me

Please contact me at miles@rout.nz.