I 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 recently figured out one way to do this that’s pretty convenient. I used code-server with selenium webdriver. Use code-server ( https://hub.docker.com/r/codercom/code-server ) …

In rust, you implement Distribution<SomeType> for Standard (from crate rand) to implement random generation of data structures. Things get messy if the data structures are recursive however. One needs to thread state down so that recursive structures are bounded. This pattern wasn’t obvious to me on first glance so I’m…

Relating to coq proofs if your frame of reference is idris. I wanted to expand my reptoire and know more proof systems, so I took this weekend to learn coq. I’m not as passable in it as idris yet, but there were some parts of its metaphor that I don’t…

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 answered via anecdotes and examples in the book. One thing I haven’t seen anyone talk about (even to the point people on mailing lists _discourage_…

It 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 a member of a Vect with zero elements (as mod used under the hood is not total for 0 anway)…

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+: I’ve been following Gabriella Gonzalez’ HasCal for a while, and decided to spend a…

Among 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 stops being particularly helpful in those cases, giving the weird feeling that you’re just on your own. In some cases you can provide positive proof…

I 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 mainstream language, so I was looking for a good elm-like framework. React is close to this but still tragically broken on state, so I wanted…

Sometimes you have disjoint but covering class instances for a type in idris. TLDR: you can use idris’ proof language and the curry-howard correspondence to both statically bind the instances and prove that disjoint class instance types are total in the same way that writing a total function is a…