TLA+ 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…Jan 27Jan 27
Destructure anything in rustIn rust, match expressions are really nice, but because containers don’t pass through the properties of the things they contain (except…Feb 5, 2023Feb 5, 2023
Quickie: 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…Nov 12, 2022Nov 12, 2022
Rust Quickie: random generator patternIn rust, you implement Distribution<SomeType> for Standard (from crate rand) to implement random generation of data structures. Things get…Oct 6, 2022Oct 6, 2022
How to be bad at coq if you know idrisRelating to coq proofs if your frame of reference is idris.Sep 26, 2022Sep 26, 2022
A 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…Jun 19, 2022Jun 19, 2022
Fin, 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…May 25, 2022May 25, 2022
HasCal — 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+:Apr 17, 2022Apr 17, 2022
Idris: 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…Nov 2, 2021Nov 2, 2021
Simple 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…Oct 14, 2021Oct 14, 2021
