Blog Posts

My New Year’s Resolution last year was a blog post a week. I’m pretty happy with how it went. My initial attitude is that even copying a section out of a textbook was fair game (and it still is) but once my flywheel was turning, I sort of always had something to write about.

Action Precedes Motivation.

I think one a week is about the right rate for me. Sometimes I feel like I could do 2 a week or sometimes I really need time to cook, but I think waiting too long is bad. More time to cook is a delusion of perfection. It means what I am thinking about is actually pretty complex and recording an early thought process is interesting in and of itself. I wish I had more documentation of my ideas and thoughts a decade, two decades ago.

You can see my relative rates of prolificness by year on the front page. 2023 was a very low year. It was probably because I was pretty depressed by events at work, which have since improved. Also I was writing more in the “notes” section, which I have since basically abandoned. I need more of a “top of the mind” organization than organization by big topic. Navigating into the right folders was too annoying and navigating by most recent is better.

I got on Hacker News a few times, which is fun to see the spike in traffic. I am not exactly sure the pattern. I think things closer to low level programming do better.

Knuckledragger

On Jan 1, I introduced Knuckledragger as sort of a theme project of the year. There is both a lot already here but also a lot of things have changed and evolved. I notice that when I go through my notes that I’ve been thinking this same basic idea for years of somehow making an ITP around z3py. I can see a lot of similar thoughts here https://www.philipzucker.com/programming-and-interactive-proving-with-z3py/ in 2019. I also see that actually the initial commit of Knuckledragger was Nov 2022 and it lay dormant until Dec 2023. I did not remember that.

CBMC

I had a number of cbmc posts this year. I think it’s quite a tool. Very easy to use for simple examples and impressive. Beyond actually trying to check properties of C code, I do think there is a lot of utility to having a convenient conventional programming language frontend to a symbolic / solver tool.

EGraphs

I went to copenhagen to give a talk at EGRAPHS2024 which was quite fun. I had been working on the angle of how Ground knuth bendix related to egraphs in 2023, but actually submitting and writing the talk. I’m a bit of a stressful speaker, which I deal with by preparing a lot, so preparing for that talk I think cast a shadow over a good 2 months before it. I am glad i did it, got compliments and I think it was an interesting and hopefully informative talk (They aren’t always). On the downside, I don’t have an implementation to show for it

Solvers

Misc

Other posts I really kind of liked but don’t know how to classify

Blog Posts to be Written

There are some loose ends in my notes that I think are interesting but haven’t made it to posts yet

I notice that writing is therapeutic, getting an idea out there. In addition to that, the reason an idea rots inside me is because it isn’t actually as fleshed out as I feel it it. Writing gets that process going.

Perhaps a new years resolution should be to pare down on this list.

  • Treeifying Graphs. There are piles of tricks or examples of people trying to think of graphs inductively, coinductively, algebraically.
  • Convex Field Theory - Linear to nonlinear is not the tractability barrier. It’s convex to nonconvex. Why does physics not use nonlinear but convex theories? Linear programming can be used to solve absolute values, min max or linear inequality contraints. Steepest descent for statistical mechanical or quantum integrals can expand around a unique minima.
  • Quantum Electrostatic - You can make a parametrized operator that is the field $V(x) = \frac{1}{x - \hat{x}}$ resulting from an ordinary single particle state. Kind of an interesting thing to talk about. $x$ is a parameter, whereas $\hat{x}$ is an operator.
  • Perturbation theory for random potentials ($p[V(x)]$ a probability functional for index of refraction or what have you) has a lot of the character of quantum field theory in a more mundane setting. You can actually validate via monte carlo. Lots of interesting phenomenology for random potentials.
  • Automated theorem provers applied to homotopy. You can model a surface equationally or relationally. Knuth bendix can give a normalization procedure for paths, solving homotopy equivalence or inequivalence as a decision procudre if it succeeds. This corresponds roughly to the idea of relaxing paths to some canonical one. The trick is proving that the relaxation does indeed go to a single canonical path per class of homotopy equivalent paths. How to go to higher homotopies? I don’t know.
  • Set theory in knuckledragger
  • Categorical Databases in sqlite
  • Semidecidable sets are “open” sets. They are closed under countable union. Complementing them isn’t as trivial as you’d think, like open sets. But likewise, NP sets are closed under “polynomial” union, because you can just say which witness. Whereas under intersection, you have to give all the witnesses. Finitary versions of synthetic topology. Finitary Konig’s lemma.
  • I really should have gottenb something out about geometrical theorem proving while I was running hot on it.
  • Manual translation validation with cbmc. It is kind of easier to copy by hand a small amount of assembly into cleanish C for translation validation. Sometimes this might be the right approach. CBMC won’t scale to mounds of autogenned code probably anyway.
  • The Schur Complement and domain decomposition. Radiation boundary conditions. Kleene algebra has a block method for kleene star that is quite similar to the schur complement.
  • Infinite ptrace. Lisp-3 and jumping into the debugger of debuggers. Making the metalayer lazy. Is there a realizability perspective on this?
  • The inverse method is a variation of the magic set / answer-demand transformation idea. You can encode demand for a sequent by using the subformula property. Then you go bottom up.
  • Lazy pairs in C and linear logic connectives.
  • Designing Bidirectional type systems as an optimization problem. Who is synth and who is check is a binary optimization variable. Annotation burden on a corpus of examples is the objective to minimize.
  • The simplicity frontier of compilers. How do we navigate the pareto curve of simplicity to code quality? That should be the point of declarative compilers.
  • Superposition solver on the z3py AST.
  • Legendre and Fourier transforms. Geometrical optics of scattering and the wave optics of scattering.
  • Programming by Linking. You can make a C file of many little pieces and use the linker script to compose them
  • ROP chains for reverse mode AD
  • Verilog Auto diff
  • Anyons in python
  • Demonstrate conformal symmetry of monte carlo Ising model
  • OPE and fast multipole method
  • Entropy, information flow, and parametricity. The relational model is a clever but kind of bizarre way of combinatorially dealing with correlation and entanglement. The “straightforward” way ought to be to use probabilities, cross entropies. Entropy is the canonical notion of “information”.
  • APL indexed on Ordinals. Sequences rather than sets as a foundation of mathematics. Making something a set takes work (sorting). Sequences happen more naturally. Sets are reflections of the logic by comprehension principles. The unorderedness of sets reflect the unorderedness of And and Or, but those are a pain in the ass actually if you’ve ever tried to build a system that supports AC. Syntax trees are actually ordered. In the logic, AC are actually proof burdens.
  • AProve for eBPF termination
  • Quotation of syntax for Z3. Inner solvers. Hilbert Choice
  • An API for Gaussian integration
  • AFL as a WalkSAT
  • Slotted Egraphs as a hash cons mod alpha
  • Undefinedness. Relational style, Maybe style, baked in.
  • Stochastic Equation Search. I loved how Kestrel has a performance guided stochastic extraction. Why not just fuse that back through the egraph at that point though?
  • Decompilation and Egraphs. Declarative decompilation. Decompilation as Macro Refolding
  • Staged Rationals as Fixed point. If you make the denominator compile time (and a power of two) and the numerator runtime, that is a fixed point number.
  • ARIP: Automated Reasoning in Python
  • Nand2 (Coq|Lean|Knuckledragger|EBMC)
  • Typed Assembly Language. Do something with this
  • Staged Metaprogramming in python
  • Nats, Lists, and Monads. Different Representations have equivalent versions. Hughes lists, power of two / binary, unary, trees, primes
  • Intrinsically sorted lists. Store the differences between elements as Nats.

More Physics

The only post I actually got out there this year was https://www.philipzucker.com/oscillate/ and it isn’t exactly my proudest post.

My focus on having some kind of computer code to go with things is constraining and inspiring. It gives me a concrete task. Am I going to write a post that is just “intro to quantum” or something? I doubt it.

More hand derivations. Less computer code (?).