System IG Semantics
I don’t have much time, so here’s just a quick jot. I don’t think System IG can prove this rather obvious proposition: |- GL(\a. Ga(Ka)) (\a x. x) Or translated to more conventional notation: (\a x. x) : (a : Type) -> (a -> a), the type of the polymorphic identity function. In order to [...]
Certificate Design Pattern
When working the latest incarnation of my System IG compiler, I used a thingy which I now realize ought to be characterized as a design pattern. It substantially changed the way I was thinking about the code, which is what makes it interesting. Summary: separate an algorithm into certificate constructors and a search algorithm. A [...]
Update
It has been a little while since I posted anything. So here’s a general update about my work and other aspects of my life. I’ve been passively thinking about Dana, but not doing very much significant. I have abandoned the RTS language on the grounds that it is too hard for my little mind right [...]
New game: “SpaceBattle”
Over the last week, I took a break from Dana and wrote a Geometry Wars-style action game. The main idea the game explores is virtuosity. Essentially there is so much to control that our puny human brains cannot comprehend it all for a long time; the game is engineered to have a very long learning [...]
Recent Comments