art yerkes·Jan 27, 2025TLA+ quickie: modelling rust codeOne often has mutable objects when working on network protocols. It’d be nice to be able to model these in TLA+ to check message flows but…
art yerkes·Feb 5, 2023Destructure anything in rustIn rust, match expressions are really nice, but because containers don’t pass through the properties of the things they contain (except…
art yerkes·Nov 12, 2022Quickie: testing vscode extensionsI made a vscode language server a while back but didn’t have a great way of doing CI tests on it (to prove the artifact itself works). I…
art yerkes·Oct 6, 2022Rust Quickie: random generator patternIn rust, you implement Distribution<SomeType> for Standard (from crate rand) to implement random generation of data structures. Things get…
art yerkes·Sep 26, 2022How to be bad at coq if you know idrisRelating to coq proofs if your frame of reference is idris.
art yerkes·Jun 19, 2022A short note on composition in TLA+I’ve now read Practial TLA+ thoroughly and if you’re going to do _anything_ with TLA+, you should read it. Most of your questions will be…
art yerkes·May 25, 2022Fin, Vect and restrict in idrisIt seems like a bit of a trap that restrict yields Fin (S n) for a Vect (S n) but it’s giving a type level protection from trying to access…
art yerkes·Apr 17, 2022HasCal — A promising embedding of pluscal in haskell.I’ve been interested in proof systems and proofs for a while. Recently, I took my first tiny step (a very bad example) in TLA+:
art yerkes·Nov 2, 2021Idris: Using the properties of simple constructors for equality and inequalityAmong the first question I asked anyone about idris was about proofs that end in having to prove that two things aren’t equal. Idris itself…
art yerkes·Oct 14, 2021Simple code with ts-elmish: a brass tacks explanationI wanted to make a vs-code extension that others might not simply rewrite or dismiss when seeing the inside of it not written in a…
