> All non-trivial properties of neural networks are undecidable.
hey, I don't know how to say this less directly, but: you're talking a lot about Rice's theorem in your comments, and I think you're using it way too broadly (look, I get it. It's a wild, mindblowing theorem). But it only applies when you take the claim in the piece to be much more general than it has to be, and when you take the narrow claim of the paper (current specific LLMs can be fruitfully analyzed with the tools we have), Rice's theorem just isn't at play.
The math analog is: you're right that the Halting problem says there are many unprovable things, but Lean + mathlib are still incredibly useful, and the halting theorem doesn't actually stop that.
> neural networks are algorithms
Again, that invites an interpretation that is too broad. Very concretely: any one neural network is a _single finite network that you can write as a single formula_. (Another analogy: we can't have an algorithm that solves the general quintic, but we can prove useful things about many specific quintics.)
Not just that, but we can solve quintics in the almost[1] general case to arbitrary precision, providing we are willing to accept approximate solutions.
[1] I exclude things that are truly perverse such as quintics with coefficients that won't fit on any physically realizable computer.
Back in college I played a similar game by drawing septagons with a straightedge and compass. They're not constructable, but a length within a three significant figures is easily constructed, and that's more accurate than I am with a compass.
The same combination of reasons we've been doing these kinds of heuristic implementations forever:
- people still get value off of an incomplete implementation, because we are allowed to be mindful of the issues (see, eg, UB in C++). In other words, many, many more bugs have been prevented by the borrow checker working as intended than have been caused by it working poorly. It's not particularly close.
- theory almost always moves slower than practice
The mutable state situation pointed out by the grandparent poster was a famous issue in typing SML under mutability that required serious changes in the language, see Section 4.2 here: https://smlfamily.github.io/history/SML-history.pdf
These were Turing-award caliber people figuring it out and, according to your definition, "yolo"ed it. This stuff is _hard_, and these driveby comments truly aren't helpful.
I lead a project built on Deno; it was not my call, just to be clear. Deno turned out unfortunately to be a miss and we had seen the writing on the wall. FWIW, we're moving to a much bigger Rust core program with node for JS user extensibility. (In other words, I'm not willing to risk using the deno_core crates.)
The one silver lining here is that Deno had already increased their node/npm compatibility. Migrating off of the jsr ecosystem and back to npm is going to be less painful than one might imagine. I expect present LLMs to be sufficiently good at the task, for example.
A few things off the top of my head (we've been on deno since 2022)
- They originally bet on being a TypeScript dialect that didn't quite match the expectations of node in a few small places that ended up mattering hugely.
- One of the original value propositions was "deno compile" and "deno bundle", and those never actually worked well enough to be robust for our real-world use cases (early on they didn't support TLA, then dynamic imports didn't work, then they had issues with ARM compilation)
- Then they simultaneously tried to support node syntax out of the box with npm import specifiers _and_ create a new javascript registry (jsr.io)
- At the point where we expected them to actually make their base-level ecosystem robust, they pivoted to edge compute, and then the writing was on the wall
(Sorry I missed your message for a few days). The short answer is "the GUI part of the stack doesn't exist": it's a cli tool (https://quarto.org). We have VS code integrations and other tooling support, but not built on deno.
Hey, I just wanted to say that this is, um, the fucking best.
I've been waiting for a literal decade for this, for the same reasons as the grand-parent poster. I literally had a chapter of my NSF CAREER proposal on this (failed, woof, but the reviewers were wrong! this rocks). The potential here is absurd. Eg, novel query optimizers and novel DB indexes could be created that, when connected to the right charting tools, would automatically emit efficient graphics and query results. Very, very cool work, thank you.
> Finding a tame enough special case was how Hawking discovered his radiation.
It's how it was formulated, but the radiation is far too weak to measure to know it's a real thing on an actual black hole; from this calculator, a 1 solar mass black hole has a Hawking radiation power of 9e-29 W: https://www.vttoth.com/CMS/physics-notes/311-hawking-radiati...
We do see analogous effects in physical analogues of black holes, but we don't know for sure that Hawking radiation actually comes off of actual black holes.
Worse, when they're small enough(!) to be luminous enough to actually observe, they should be hot enough to be spewing out a whole load of exotic nonsense particles (not just photons) that we don't really know how to model correctly with regards to Hawking radiation even if it is part of whatever ends up unifying QM and GR.
Given even the event horizon of a BH doesn't play well with QM, it's probably best to wait for some physicists to work out how to combine QM and GR better.
This is so cool. It's a much better version of what Bill Cheswick and I did almost 15 years ago with footage from a SFO->EWR flight: https://cscheid.net/static/windowseat/
I'm just going to answer this one candidly. Yes, you are doing something wrong. Immediately: the commit history is useful to understand the context in which a bug was introduced, because it's the best context to understand the _reason_ the mistake was maybe, which is a really good way to prevent regressions. But more generally: when an entire industry has arrived at an accepted practice, you the junior developer (sorry, 5 years is _nothing_: you need to be told this too) have a chance to pick up on it.
Have you heard "have you played guitar for 20 years, or have you played guitar 20 times for a year?" Time only helps with accumulating wisdom if you let it.
Seriously, though, there's one nomogram you (yes you) should know about and have it well-enough engraved in your mind's eye that you can use it with eyes closed. A nomogram for Bayes' theorem: https://www.ovid.com/journals/nejm/abstract/10.1056/nejm1975...
That is cool, although it took me awhile to understand it because the posterior probability is on the left and the prior probability is on the right, and because it uses D=Disease and T=Test when I am used to seeing D=Data.
You're right that I can't reproduce it like a phone camera could, and that the more precise you are the better (and it might be that with my eyes closed I'm doing something closer to addition in log-odds, like a separate comment responded), but this is super useful even coarsely. The visual affordance gives Bayes's theorem a physicality unlike any other tool I've found.
reply