cmrx64

i consider it the root menu of the phone

i got so inspired by reading diaspora this year that i instantly started working on some polisware. cipherclerk operational: https://github.com/emberian/dregg

topical to the conversation, it is fully formally verified in lean (with some UC security reductions done in isabelle). also did this in HOL4 inspired by some work i did with ramana kumar in 2016, on reflective self-verifying self-modifying systems: https://github.com/emberian/svenvs

it is unlikely that other mosquitos (that don’t carry disease) will fail to fill the niche

thinking about how to communicate it in a clear way. “the control knobs of what actually makes us different from one another” — you don’t expect one of your kids to be quadripedal. otoh this doesn’t really capture the precise notion either.

The Electronic Harpsichord, same year. must have been an interesting time.

LLM API endpoint does do compaction. OpenAI definitely does support serverside compaction, both explicit and automatic, and this is different than what could be implemented purely clientside: https://developers.openai.com/api/docs/guides/compaction (and there was rumors a few months ago on HN about how activation-preserving/latent it is, vs just summarization). Anthropic as well, in beta (new to me): https://platform.claude.com/docs/en/build-with-claude/compac...

and soon from space? radio engineering breakdown of starlink radar capabilities, it’s a pretty impressive bird if you were designing it only for that: https://youtu.be/jbp3kdJZ1_A

four figures these days. fits in your hand. nanopore is a revolution. https://nanoporetech.com/products/sequence/minion

there’s youtubers that have videos about doing this in a home wetlab. very achievable. some amateur soil biologists using this to try and sample microdiversity as the planet… humanifies.

i think of them as tiers of expertise— need to master the basics of structure and form before the robot has the learned representations to competently model user interactions with more fluid instantiations (by downprojecting into the overlearned fixed-semantics)

claude-opus-4-7

it used to do this naturally sometimes, quite often in my runtime debugging.

Dijkstra would shake his head at our folly.

quite interested; email in bio.

Those offices themselves were liminal (in sense of ritual) in a way, providing the threshold for the information age to take root.

this is a pretty bad vfs. there are pure “cap manifest” approaches that don’t pull in decades of cruft semantics. don’t build systems that aren’t objectstore native in 2025 (since this work was initiated in december).

meh. i’ll keep using scrapinghub.

https://hellas.ai is building out their category theoretic compiler and protocol for solving this issue

RIP

aodv works great and is “actual mesh.” the ‘overlays’ scale in practice and are topology agnostic, the hierarchical bgp mesh underneath isn’t altering the message or memory complexity, we can talk about them as algorithms. there are 10ks node meshes in the real world that use batman, geography-contrained hub and spoke, etc. guifi has 37k nodes in its heterogenous mesh with a batman fork, freifunk (originator of batman) around 40k.

edit to add: what is observed in practice is that gossip protocols can’t coordinate peers without centralizing. this is natural, and an artifact of the logarithmics in the routing protocols. the appropriate thing to do is model routing as a revocable proof system, and information theory explains the centralizing dynamics (problem I worked on 2018-2019) https://eprint.iacr.org/2022/1478 proves the global lower bound is linear (in route updates, when applied to routing, naively quadratic if distributed), and the trick routing protocols add to the game is locality, which yields the logarithmic advantage that when multiplied across the entire network is substantially subquadratic.

this isn’t a theorem of network science, and is an easily avoided failure mode. plumtree? kad? aodv? you’re wrong :(

this feels a bit like a bombshell given the other recent works on emergent misalignment. how long have we been lying to models?

What tasks are in your sights for evaluating the approach? is there anything you are most excited/curious to see the approach demonstrate?

Contrariwise, I was part of the troupe of people that daily picked up these bags along walking trails. One of the few benefits of living in the USA: covert prosocial behavior is extremely common.

smell isn’t integrated in the thalamus with other sensory streams, it does something else entirely

A decade ago I ran several “seven hour roguelikes”, https://web.archive.org/web/20160321153532/http://people.cla... is the documentation from the first one.

The first year I spent six hours writing one of the first ecs crates in Rust and then an hour turning it into a game. lots of fun! you can search “7HRL” on github to find the historical participants not too ashamed to publicize their code at the end. A few dozen people enjoyed this.

List.TFAE is a helper definition and it’s invoked on a funny looking term when translated directly into english. I don’t know what I think, yeah it’s kinda junky but not in the way that 57 \mem 100 in a set encoding of the naturals.

    theorem TFAE_7_binary : List.TFAE (7).bits := by
  unfold Nat.bits Nat.binaryRec Nat.binaryRec; simp!

the binary expansion of 7 has three elements (you will find them at indexes Fin 0, Fin 1, and Fin 2) and the proof is of their equality.

the last paragraphs cite why junk theorems are objectionable but then fully misinterprets it to draw the opposite conclusion. the intersection is the S-feature and problematic. 1 + 2 = 4 is a “theorem beyond T” expressed in T theory.

don’t be mislead about what a junk theorem is!

rtld does a lot of work even in “static” binaries to rewrite relocations even in “unused parts” of any PIE (which should be all of them today) and most binaries need full dyld anyway.

That would deliver a blow to the integrity of the rest of that section because those sorts of upper bound constraints immediately reducible to “true” cannot cause backtracking of any kind.