tel

An assert statement requires that you specifically come up with a test case. Lean lets you verify for all possible cases. Infinity is not a problem.

It's similar to a type system in that regard. The same difference could be applied there (comparing a Python type assert). Types, however, generally only cover checks similar to "the shape of the data is X".

Lean is different in that its language for expressing properties is wide enough to express anything you can imagine. The bottleneck becomes accurately stating properties you'd like to enforce and, subsequently, discovering proofs of whether or not they're true.

Without having any opinion on whether or not the Bun team was meaningfully fuzzing their codebase... Andrew's claim was not about whether or not they were, it was noting that the story was different between what they claimed in conversation and what they stated in this article.

It's also a language of distancing from personal experience and honesty.

Not saying you're wrong. Professionalism is an important tool for maintaining professional relationships. Lack of professionalism is dangerous to the point where it is reasonable for certain kinds of societies to begin to shun people who don't engage with it.

And, at the same time, a certain amount of emotional honesty can be really important to share, too. And that includes some amount of judgement and criticism.

It sounds like Zig's relationship with Bun is over. While Anthropic/Jason/Bun did not write a personal narrative about the end of that relationship, they absolutely were the initiators and could not have done this in a more aggressive way. It feels to me to be approximately the equivalent of moving out in secret and serving the divorce documents through your lawyer.

I think you've got it. You go in each day and work on things and talk with people working on things. There are multiple opportunities to share weekly, one or two are pretty regular and the rest are self-organized. Maybe you learn about something new and dive in, maybe you come up with a project and share it with others.

I think the beating heart is that everyone is there with some passion to learn and build and you're encouraged to do so collaboratively. It's surprising, I feel, how rare it is to have a community of folks who are all learning together and not afraid to dive in and figure things out. Recurse Center is a chance to spend 6 or 12 weeks building and then living in a place like that.

I'm working on an easy-to-embed typed language called Ekto. I am taking a lot of inspiration from Koka and aiming to support full multi-shot delimited continuations all while keeping the virtual machine deeply predictable from the host side.

I'm also rebuilding an integrated task/knowledge/publication system I'd previously built atop Gemini's Gemtext format. While I loved the simplicity, I've discovered that there are lots of burrs in that design, especially on the publication side, which I'd be able to lift by using a more fully featured document format like Djot.

I was asking questions about compiler techniques. Then when I got annoyed I started asking about experimental design. Both were very frustrating experiences once I started realizing how limited its responses were.

Though yeah the edgelord-y style faded after I criticized it a couple times.

All my usage of Grok for technical topics shows it regularly deeply misunderstanding things and just parroting back my question in fancy language. It’s the only frontier model I get this impression of. That makes it super annoying when it tries to market itself as good at engineering tasks when it seems (to me) to be much worse at them.

I think, yes, with greater splat density—and, critically, more and better inputs to train on, others have stated that these performances were captured with 56 RealSense D455fs—then splats will more accurately estimate light at more angles and distances. I think it's likely that during capture they had to make some choices about lighting and bake those in, so you might still run into issues matching lighting to your shots, but still.

https://www.realsenseai.com/products/real-sense-depth-camera...

That said, I don't think splats:voxels as pixels:vector graphics. Maybe a closer analogy would be pixels:vectors is the same as voxels:3d mesh modeling. You might imagine a sophisticated animated character being created and then animated using motion capture techniques.

But notice where these things fall apart, too. SVG shines when it's not just estimating the true form, but literally is it (fonts, simplified graphics made from simple strokes). If you try to estimate a photo using SVG it tends to get messy. Similar problems arise when reconstructing a 3d mesh from real-world data.

I agree that splats are a bit like pixels, though. They're samples of color and light in 3d (2d) space. They represent the source more faithfully when they're more densely sampled.

The difference is that a splat is sampled irregularly, just where it's needed within the scene. That makes it more efficient at representing most useful 3d scenes (i.e., ones where there are a few subjects and objects in mostly empty space). It just uses data where that data has an impact.

Gaussian splatting is a way to record 3-dimensional video. You capture a scene from many angles simultaneously and then combine all of those into a single representation. Ideally, that representation is good enough that you can then, post-production, simulate camera angles you didn't originally record.

For example, the camera orbits around the performers in this music video are difficult to imagine in real space. Even if you could pull it off using robotic motion control arms, it would require that the entire choreography is fixed in place before filming. This video clearly takes advantage of being able to direct whatever camera motion the artist wanted in the 3d virtual space of the final composed scene.

To do this, the representation needs to estimate the radiance field, i.e. the amount and color of light visible at every point in your 3d volume, viewed from every angle. It's not possible to do this at high resolution by breaking that space up into voxels, those scale badly, O(n^3). You could attempt to guess at some mesh geometry and paint textures on to it compatible with the camera views, but that's difficult to automate.

Gaussian splatting estimates these radiance fields by assuming that the radiance is build from millions of fuzzy, colored balls positioned, stretched, and rotated in space. These are the Gaussian splats.

Once you have that representation, constructing a novel camera angle is as simple as positioning and angling your virtual camera and then recording the colors and positions of all the splats that are visible.

It turns out that this approach is pretty amenable to techniques similar to modern deep learning. You basically train the positions/shapes/rotations of the splats via gradient descent. It's mostly been explored in research labs but lately production-oriented tools have been built for popular 3d motion graphics tools like Houdini, making it more available.

Definitely not common! Nice to hear I'm not alone either.

And yeah, I agree. Practically, it's the thing that annoys me the most day-to-day. I've mostly got wrapping set up to handle it now, but it remains a little finicky.

I've recently begun replacing Markdown with Gemini's .gmi/gemtext format. It is Markdown with fewer features. I appreciate the simplicity and it's tremendously easy for custom tools to parse.

It has no inline formatting, only 3 levels of ATX headers (without trailing #s), one level of bullet points using only asterisk and not dash to delimit, does not merge touching non-whitespace lines (thus expecting one line per paragraph), and supports only triple-backtick fenced preformatted text areas that just flip on and off.

Maybe the biggest change is that links are necessarily listed on their own line, proceeded by a `=>` and optionally followed by alt-text.

My gemtext parser is maybe 70 lines and it is arguably 95% of what one needs from Markdown.

SDFs still scale by geometry complexity, though. It costs instructions to evaluate each SDF component. You could still use something like BvH (or Matt Keeter’s interval arithmetic trick) to speed things up.

Genuine question, how does SPIR-V compare with CUDA? Why is SPIR-V in a trench coat less desirable? What is it about Metal that makes it SPIR-V in a trench coat (assuming that's what you meant)?

At the same time, if you want to use Claude to read the source and narrate how it works to you that’s trivial to do as a user.

If you're familiar with Zorn's Lemma, the construction is just to order bases by inclusion and to consider chains created by noting that there must be an independent dimension and adding it inductively. You can upper bound each of these chains by unioning the members of the chain (which preserves linear independence). By Zorn's Lemma that means there is a maximal linearly independent system and if an element existed outside of that system's span it would contradict that maximality.

Yeah, that's correct. You also often see it as having that for any method `X -> T<Y>` there's a corresponding method `T<X> -> T<Y>`. Or you can have that for any two arrows `X -> T<Y>` and `Y -> T<Z>` there's a composed arrow `X -> T<Z>`. All are equivalent.

Every monad is also an applicative and liftA2 does/is the same thing as liftM2. The only reason they both exist was due to Monad being popularized in Haskell earlier than Applicative and thus not having it as a superclass until the Functor-Applicative-Monad Proposal in Haskell 2014. It was obviously correct, but a major breaking change that also got pork barreled a bit and so took a while to land.

Monad tutorials are on the rise again.

Let's start with function composition. We know that for any two types A and B we can consider functions from A to B, written A -> B. We can also compose them, the heart of sequentiality. If f: A -> B and g: B -> C then we might write (f;g) or (g . f) as two different, equivalent syntaxes for doing one thing and then the other, f and then g.

I'll posit this is an extremely fundamental idea of "sequence". Sure something like [a, b, c] is also a sequence, but (f;g) really shows us the idea of piping, of one operation following the first. This is because of how composition is only defined for things with compatible input and output types. It's a little implicit promise that we're feeding the output of f into g, not just putting them side-by-side on the shelf to admire.

Anyway, we characterize composition in two ways. First, we want to be clear that composition only cares about the order that the pipes are plugged together, not how you assemble them. Specifically, for three functions, f: A->B, g: B->C, h: C->D, (f;g);h = f;(g;h). The parentheses don't matter.

Second, we know that for any type A there's the "do nothing" identity function id_A: A->A. This doesn't have to exist, but it does and it's useful. It helps us characterize composition again by saying that f;id = id;f = f. If you're playing along by metaphor to lists, id is the empty list.

Together, composition and identity and the rules of associativity (parentheses don't matter) and how we can omit identity really serve to show what the idea of "sequences of pipes" mean. This is a super popular structure (technically, a category) and whenever you see it you can get a large intuition that some kind of sequencing might be happening.

Now, let's consider a slightly different sort of function. Given any type types, what about the functions A -> F B for some fixed other type F. F here exists to somehow "modulate" B, annotate it with additional meaning. Having a value of F B is kind of like having a value of type B, but maybe seen through some kind of lens.

Presumably, we care about that particular sort of lens and you can go look up dozens of useful choices of F later, but for now we can just focus on how functions A -> F B sort of still look like little machines that we might want to pipe together. Maybe we'd like there to be composition and identity here as well.

It should be obvious that we can't use identity or composition from normal function spaces. They don't type-check (id_A: A -> A, not A -> F A) and they don't semantically make sense (we don't offhand have a way to get Bs out of an F B, which would be the obvious way to "pipe" the result onward in composition).

But let's say that for some type constructors F, they did make sense. We'd have for any type A a function pure_A: A -> F A as well as a kind of composition such that f: A -> F B and g: B -> F C become f >=> g : A -> F C. These operations might only exist for some kinds of F, but whenever they do exist we'd again capture this very primal form of sequencing that we had with functions above.

We'd again capture the idea of little A -> F B machines which can be plugged into one another as long as their input and output types align and built into larger and larger sequences of piped machines. It's a very pleasant kind of structure, easy to work with.

And those F which support these operations (and follow the associativity and identity rules) are exactly the things we call monads. They're type constructors which allow for sequential piping very similar to how we can compose normal functions.

The more constrained your theory is, the fewer models you have of it and also the more structure you can exploit.

Monads, I think, offer enough structure in that we can exploit things like monad composition (as fraught as it is), monadic do/for syntax, and abstracting out "traversals" (over data structures most concretely, but also other sorts of traversals) with monadic accumulators.

There's at least one other practical advantage as well, that of "chunking".

A chess master is more capable of quickly memorizing realistic board states than an amateur (and equally good at memorizing randomized board states). When we have a grasp of relevant, powerful structures underlying our world, we can "chunk" along them to reason more quickly. People familiar with monads often can hand-wave a set of unknowns in a problem by recognizing it to be a monad-shaped problem that can be independently solved later.

I’m not a huge fan of these, but this time I noticed that the best ones feel a lot like naturality arguments. As in, moving structural bits in a way that makes it clear that we’re not touching anything that ought to be universally quantifiable.

I still don’t love this sort of thing being presented as “proof”, but I thought that idea is interesting. Is there a way to formalize naturality into technical diagrams? Probably!

Often it's easy to construct a family of sets representing something of interest. For example, we like to define integration initially as a finite process of breaking the integrand's domain into pieces, computing their area, and summing.

To compute the contribution of some piece indexed i, we measure the size of its domain, call it the area Ai, and then evaluate the integrand, f, at some point xi within that domain, then the contribution is Ai * f(xi).

Summing all of these across i produces a finite approximation of the integral. Then we take a limit on this process, breaking the domain into larger and larger families of sets with smaller and smaller areas. At the limit, we have the integral.

This process seems intuitive, but it contains an application of the axiom of choice---in the limit, we have an infinite number of subsets of our domain and we still have to pick a representative xi for each one to evaluate the integrand at.

It's quite obvious how to pick an arbitrary representative from each set in a finite family of sets: you just go through one-by-one picking an element.

But this argument breaks down for an infinite family. Going one-by-one will never complete. We need to be able to select these representative xis "all at once". And the Axiom of Choice asserts that this is possible.

(Note: I'm being fast-and-loose, but the nature of the argument is correct. This doesn't prove integration demands AoC or anything like that, just shows how this one sketch of an argument would. Specifically, integration normally avoids AoC because we can constructively specify our choice function - for example, picking the lexicographically smallest point within each axis-aligned rectangular cell. Generalize to something like Monte Carlo integration, however...)

The quantification over T is still kind of weird, though. In a formulation like `for all T, (T and P consistent and T and neg P consistent)` is trivially false, just take `T = {neg P}` and now `{P, neg P}` is inconsistent.

We're never trying to show P is independent of all theories, just some specific one.

Yeah, I agree. "Independence" is fundamentally a property of the formal system you're working within (or really, it's a property of the system you're using and of the axiomatic system under test, the system a proposition would be independent from). I'm holding out a bit to unify that with "undecidability" because undecidability takes on a particular character in constructive systems that happens to align with Turing's notion.

So at some level, this was just an acknowledgement that "undecidability" in this form is well represented in formal logic. In that sense, at least in constructive logics, it's not just a synonym for "independence".

Quantifying over T is probably not going to work. In informal terms that reads like "No logic exists where P is independent", which probably wasn't quite what you wanted, but also we can trivially disprove that with T = {}. As long as P is self-consistent, then "not P" should be too.

We're interested in a proposition's status with respect to some theory that we enjoy (i.e. Zermelo–Fraenkel set theory).

Independent and undecidable aren't quite the same, even in formal logic. Or rather, sometimes they are but it’s worth being specific.

A proposition P being independent of a theory T means that both (T and P) and (T and not P) are consistent. T has nothing to say about P. This may very well be what Gödel was indicating in his paper.

On the other hand, undecidable has a sharper meaning in computation contexts as well as constructive logics without excluded middle. In these cases we can comprehend the “reachability” of propositions. A proposition is not true or false, but may instead be “constructively true”, “constructively false”, or “undecidable”.

So in a formal logic without excluded middle we have a new, more specific way of discussing undecidability. And this turns out to correspond to the computation idea, too.

I really like TAPL but would recommend Harper’s Practical Foundations of Programming Languages (PFPL) first (though skip the first 2 chapters I think?).

https://www.cs.cmu.edu/~rwh/pfpl.html

It’s far more directed than TAPL, so I think it’s easier to read from start to finish. TAPL feels better as a reference.

Sorry, Haskell’s “monad transformer library”. One of the earliest approaches to composability of multiple monadic effects. It’s pretty similar to an algebraic effect system allowing you to write effectual computations with types like `(Error m, Nondet m, WithState App m) => m ()` to indicate a computation that returns nothing but must be executed with access to error handling, nondeterminism, and access to the App type as state.

There are a few drawbacks to it, but it is a pretty simple way to get 80% of the ergonomics of algebraic effects (in Haskell).

They're pretty similar, but with different ergonomics. Algebraic effects are similar to some kind of "free" monad technique, but built in. For being built in they have nicer syntax and better composability, often. You can achieve the same in a language suitably dedicated to monadic approaches (Haskell being the poster child here) but it helps to have type class inference (giving you mtl-like composability) and built-in bind syntax a la Haskell's `do` or Scala's `for`.

I would also always use that in a mathematical context but feel it’s weird to hear, say, “proved in a court of law”.

Looking around, here's a post by the author on Twitter where he shows similar motion and states that the time-lapse is 10m at 1min/sec.

https://x.com/mag2art/status/1385940103189745669