### Quiet Nights and Quiet Stars

Six month retrospective on thinking small. I describe work optimizing GHC backend like LLVM, conversion of Paul Tarau’s bijective Godel numbering to term algebras in regular shape polymorphic parallel arrays library. I note Vladimir Veovodsky’s interest in Martin-Lof Type theory. And Agda as a potential target implementation for univalent foundations in mathematics.