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. …

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. …

why things are kind of awful and perhaps a way toward away from awfulness tldr; Often, we’re working to a deadline that should be a “delivery timebox”, and our narrow focus on “outcomes” often blinds us to the ways we can get more smarter without breaking everything. My theses: We…

I wanted alists with guaranteed unique values, and finally decided to sit down and work out how this functions in idris. For those not as old as dirt, an alist in lisp is a list of pairs where the (car) of each is considered to be the key, so it…

prozacchiwawa/idris-subleq Subleq.SubleqMachine pc mem encodes the full state of the computer in its type, so it should be possible to ask idris…github.com Two things I learned from this: If you write objects with values encoded at both runtime and compile time, you can use type classes to guide Idris through induction on them rather than having to reimplement it as proof code. Not only that, but the compiler can act as a…