George Brown g0xA52A2A

Solving SAT via interaction net superpositions

I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite

This is the predecessor of Mazeppa.

Supercompilation is a deep program transformation technique due to V. F. Turchin, a prominent computer scientist, cybernetician, physicist, and Soviet dissident. He described the concept as follows [^supercompiler-concept]:

A supercompiler is a program transformer of a certain type. The usual way of thinking about program transformation is in terms of some set of rules which preserve the functional meaning of the program, and a step-by-step application of these rules to the initial program. ... The concept of a supercompiler is a product of cybernetic thinking. A program is seen as a machine. To make sense of it, one must observe its operation. So a supercompiler does not transform the program by steps; it controls and observes (SUPERvises) the running of the machine that is represented by th

Check Out these projects, papers and blog posts if you're working on Geo redundant Datacenters or even if you only need to have your software hosted there. It's good to know what you're in for.

  Collected these for a colleague, these have been super useful over 
  the past 15+ years and and will most likely help and/or entertain you. 
  May be extended in the future.
  -- azet (@azet.org)

load balancing

DNS geo & anycast

I get asked pretty regularly what my opinion is on merge commits vs rebasing vs squashing. I've typed up this response so many times that I've decided to just put it in a gist so I can reference it whenever it comes up again.

I use merge, squash, rebase all situationally. I believe they all have their merits but their usage depends on the context. I think anyone who says any particular strategy is the right answer 100% of the time is wrong, but I think there is considerable acceptable leeway in when you use each. What follows is my personal and professional opinion:

Parallel Python within the same process or hacking around the cursed GIL with a hand-rolled library loader

From its obscure beginnings in Amsterdam, the Python programming language has become a fundamental building block of our digital society. It is used literally everywhere and by everyone for a mind-boggingly wide variety of tasks.

Python is also the lingua franca of Data Science, tying together tools for data loading, wrangling, analysis and AI. There is a massive ecosystem of contributed Python packages, which - for example - allows reading every obscure data format under the sun. This makes Python and its ecosystem extremely valuable for analytical data management systems: Users are likely somewhat familiar with Python due to its immense popularity and the ecosystem provides solutions for most data problems. As a result, Python is being integrated into SQL systems, typically through so-called User-Defined Functions (UDFs). For example, [Apach

Cache Oblivious and Cache Aware Data Structure and Algorithms

Cache-Oblivious Algorithms and Data Structures - Erik Demaine (One of the earliest papers in cache oblivious data structures and algorithms that introduces the cache oblivious model in detail and examines static and dynamic cache oblivious data structures built between 2000-2003)
Cache Oblivious B-Trees - Bender, Demaine, Farch-Colton (This paper presents two dynamic search trees attaining near-optimal performance on any hierarchical memory. One of the fundamental papers in the field where both search trees discussed match the optimal search bound of Θ(1+log (B+1)N) memory transfers)
Cache Oblivious Search Trees via Binary Trees of Small Height - Brodal, Fagerberg, Jacob (The data structure discussed in this paper works on the version of [2] but avoids the use o

	{
	"$schema": "https://zed.dev/schema/themes/v0.1.0.json",
	"name": "Blanche",
	"author": "OJ Kwon<[email protected]>",
	"description": "Naive port for the VS code theme Blanche https://marketplace.visualstudio.com/items?itemName=shytikov.blanche . Credits to https://github.com/shytikov/blanche",
	"themes": [
	{
	"name": "Blanche light",
	"appearance": "light",
	"style": {

	const assert = @import("std").debug.assert;

	fn compressBlock(writer: anytype, src: []const u8) !void {
	var table = [_]u32{0} ** 4096; // size is pow2. bump to match more. ideal = (0xffff+1) / sizeof(u32)
	var anchor: u32 = 0;

	if (src.len > 12) { // LZ4 spec restriction: last match must start 12b before end of block.
	var pos: u32 = 0;
	while (pos + 4 < src.len - 5) { // LZ4 spec restriction: last 5b are always literal.
	const blk: u32 = @bitCast(src[pos..][0..4].*);

	"""
	DISCLAIMER: This is a quick prototype, it's not at all tested, and may be deeply cryptographically flawed.

	Normally, JSON canonicalization is at least O(nlogn), because you need to sort the map keys.

	This approach avoids the need to do that, and in theory it's O(n), but in practice it's probably slower for most inputs... I have not benchmarked.

	If you limit recursion depth, you could implement it as an Online Algorithm https://en.wikipedia.org/wiki/Online_algorithm

	NB: Python's JSON parser allows duplicate map keys, which this impl will be oblivious to.

	// A nano dependent type-checker featuring inductive types via self encodings.
	// All computation rules are justified by interaction combinator semantics,
	// resulting in major simplifications and improvements over old Kind-Core.
	// Specifically, computable annotations (ANNs) and their counterpart (ANN
	// binders) and a new self encoding based on equality (rather than dependent
	// motives) greatly reduce code size. A more complete file, including
	// superpositions (for optimal unification) is available on the
	// Interaction-Type-Theory repository.
	// Credits also to Franchu and T6 for insights.