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.
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)?
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.
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!
[ my public key: https://keybase.io/tel; my proof: https://keybase.io/tel/sigs/hy256UGUMMtc9NhfOsck4vuCiby6UYNLw7VXBj4fGR8 ]