art yerkesDestructure anything in rustIn rust, match expressions are really nice, but because containers don’t pass through the properties of the things they contain (except…3 min read·Feb 5, 2023----
art yerkesQuickie: 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…1 min read·Nov 12, 2022----
art yerkesRust Quickie: random generator patternIn rust, you implement Distribution<SomeType> for Standard (from crate rand) to implement random generation of data structures. Things get…2 min read·Oct 6, 2022----
art yerkesHow to be bad at coq if you know idrisRelating to coq proofs if your frame of reference is idris.5 min read·Sep 26, 2022----
art yerkesA 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…6 min read·Jun 19, 2022----
art yerkesFin, 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…2 min read·May 25, 2022----
art yerkesHasCal — 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+:2 min read·Apr 17, 2022----
art yerkesIdris: 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…3 min read·Nov 2, 2021----
art yerkesSimple 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…2 min read·Oct 14, 2021----
art yerkesType classes in idris: proving away constraints and ensuring totalitySometimes you have disjoint but covering class instances for a type in idris. TLDR: you can use idris’ proof language and the curry-howard…3 min read·Jun 8, 2021----