Dana (actual) progress

I have some very exciting news! I wrote some actual code in the Dana repository. It is the IΞ Certificate module. That is, it’s an abstract data type Proof, such that only valid proofs in IΞ can be constructed.
The certificate module (IXi.Term and IXi.Proof together) is about 280 lines, which isn’t fantastically [...]

Some Constructions in IΞ

Over the past couple months, I have been attempting to find a language to use as a core calculus for Dana, as anyone who follows this blog knows. I have been slowly converging on IΞ for its elegance and simplicity. It turns out to be very powerful, capable of modeling many structures while [...]

Might as well face it, I’m addicted to logic

I’m trying really hard not to become a logician. Like my obsession with FRP, it would be very interesting and educational. But my FRP fancy came from a desire to make games more easily, and I have since lost interest in that endeavor, studying FRP for its own sake. Now I am [...]