The structure of Lean does impose that. The code isn't being run, it's being type checked. And that's it. The overwhelming majority of Lean code is never run. It exists only to be type checked (because type checking is equivalent to verifying the proof).
You could imagine the typechecker has bugs (and indeed another comment mentions examples of bugs!). Crucially though anytime the typechecker has a bug fixed you could rerun the typechecker on the code to see if it still type checks.
This is the whole promise of formal verification. It reduces the problem of verification purely to the typechecker. If the typechecker is correct, then the proof is verified, no matter how many lines of code the proof is. As a sibling comment puts it, the chance of bugs mainly scales with the number of lines of code in the typechecker, not in the amount of lines of Lean code.
Your question is akin to asking, "yes this spellchecker ran fine on your essay, but are you sure it runs fine on War and Peace? That's 1000x more words!" To which the answer is the number of words doesn't matter if the spell checker is correct (which it might not be! And longer passages might reveal more bugs! But you can always rerun it). The main source of bugs is more lines of code in the spell checker, not in number of words in the text.
> Astra’s progress helps clarify which AI capabilities are out of reach and which questions remain open.
Okay. But I don't think this entire article at all explained which AI capabilities remain out of reach. Did I miss something? Other than "oh I guess it could still get even more superhuman on ARC-AGI-3 than it is?"
> It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.
Generally you only need to look at 10-100 lines (unless you have a highly novel theorem that essentially invents a new field of math or builds on a field that has never been worked on in Lean before) of the 250k to verify what it claims. This is why there is excitement around formal verification. The rest of it is perhaps useful to read to figure out why the proof works, but is not necessary for checking.
That paper has had a pretty turbulent reception and looks pretty conclusively wrong at this point.
It used an incorrect theoretical framing that assumed that data was being replaced rather than accumulated as a result of more training (see https://arxiv.org/abs/2404.01413 which explores this). This is incorrect because this simply isn't how real-world datasets are created via synthetic data generation (which generally accumulate more data over time rather than replace their data). As a result most of the theoretical results were invalid.
Empirical evidence has also cast a considerable amount of doubt on the paper. For example, Microsoft Phi-4 was an empirical test in specifically what happens if the majority of your training data is synthetic rather than human and it turns out that Phi-4 did significantly better than previous models which relied primarily on human data.
There's some nuance to all of this in how exactly you do this, but the original claims of the paper are looking really shaky at this point.
> GPT-4(?) was capable of beating Pokemon 18 months ago but models only became capable of beating it without a harness in the last six months...?
GPT-4 was decidedly not capable of beating Pokemon 18 months ago. I doubt it would be able to complete a single level. I don't think people realize how large the advances in model capabilities have been. GPT-4 in a modern harness is absolutely horrendous compared to modern models.
Yes. Presumably you're referring to my use of the word "level". I mean here basically every "level" as denoted by the order of locations and places on the town map that you get (which is usually +- some other locations how game runners refer to different sections of the game).
Still might be viable, but would be tricky to sell.
> SUBSCRIPTION TERMS
> This license is subscription-based and will remain valid only for the duration of your active subscription. Upon expiration or termination of your subscription:
> a) Your rights to use the Software will cease; b) You must uninstall and stop using the Software; and c) You may lose access to any data or content created with or stored in the Software.
On the other hand, norms in software right now are that suckers build and maintain software for free + "the love of the game should be enough for anyone", so it's shocking when people break the norm.
That's not the norm that's being broken here. Most DB technologies provide a "pay for updates, if you stop paying you keep the last version you paid for" model. This is how Oracle prices its DB tech, this is how jOOQ is priced (which is probably the closest thing to Acadia), this is how MS prices its DB tech etc.
The responses to the pricing aspect of this announcement around the web disagree.
I'm not saying you can't find paid software, especially from Oracle and Microsoft, but there's a different expectation for "just-a-guy announcing his project on twitter".
You can see a similar mentality regarding Elm in general where the approachability of one guy had people in some sort of parasocial entitlement to the project that you wouldn't see if, for example, it were Google or an unknown who built Elm.
No, not at least for Photoshop. If you have the subscription version and fail to pay it downgrades you to the free version which has more limited editing capacity but still has read capacities.
More broadly I think the only subscription products most software developers are used to where access to data is revoked is cloud infra. Most software stuff follows models like Jetbrains (where e.g. you pay for updates but keep the oldest version). E.g. this is how things like SQL Server or other paid DB technologies work, where you effectively are subscribing to yearly updates, but get to keep the current version if you stop paying the subscription fee.
I'm wary of languages that seek to own the database. In particular, the claim "Coexist with SQL" seems a bit suspect given that e.g. sum types have a custom binary encoding, which likely makes them difficult to interop with from other languages. This makes the claimed interop with other languages really more of a temporary stopping point towards full Acadia adoption rather than a viable long-term equilibrium, unless you e.g. eschew using sum types. (I also suspect that trying to natively support sum types can lead to a kind of FP-equivalent of ORMs' impedance mismatch. The ways I model data with relational logic can be pretty different than the ways I model data with algebraic datatypes and I wonder if trying to force fit the latter into the former doesn't lead to the same problems as force fitting objects into relational logic).
This makes the database closer to something that Acadia compiles to, rather than something Acadia sits on top of. From my own developer experience this feels off, because I generally expect the data layer to be king and application code to revolve around that, rather than having data representation created in code and the database created off that (this is why I also dislike things like ORMs).
In general I view databases as usually having more longevity than application code, especially as you accumulate more data over time. For serious production applications, the database often outlives multiple rewrites of the production application.
I suspect though my concerns are overall rather minor. The ergonomics of the language itself seem enjoyable. Acadia seems like it would be great as an embedded DSL. It's a bit unfortunate that it currently seems coupled to creating an HTTP server. I think that Acadia has greater ambitions beyond just the database, as evidenced by creating a binary web connection with frontend Elm code to presumably obviate the need for encode-decode layers. It seems like Acadia is meant to be a stepping stone towards a closer frontend-backend fusion. But I agree with mjaniczek that something like Lamdera seems a better fit for that.
But given how early Acadia is, I'm still very excited for where it goes. What I've listed is surmountable and I also feel that often a closer frontend-backend fusion might be worthwhile.
I think, the reality is SQL being simply to old to coexist with a web app use case. All the nice things that article talks about are not possible to nicely integrate with SQL. Current development is done by either writing SQL by hand or by letting ORMs to autogenerate it. Both feel bad because of how bad SQL is. But there is no other option. I hope https://substrait.io/ will gain traction and will be supported natively by databases
Just as with any kind of programming I want to be able to detect as much amount of issues as early as possible. That includes issues like invalid queries (both on syntax and types level) but also stuff like will specific transaction isolation level be just enough (from correctness and performance point) for my specific use case, or will the migration query lock the whole db or take multiple days to execute because I didn't know some niche quirk. To me it is obvious that you will not beable to do that with SQL, one because it is old so it accumulated all the weird quirks, that were done in the name of backward compatibility, two is that by it's nature of being script language you just could not do more complicated cross query static analysis. See also https://www.scattered-thoughts.net/writing/against-sql which nicely describes other issues. See languages like PRQL for better syntax, or https://www.languagesforsyste.ms/MixT/ for static analysis possibilities
I am mostly aligned with the article on what I want from next generation of web development. But I don't think using specific library in a specific language or specific query language is a viable long term solution. Hance the mention of Substrait. The solution that I think is needed, is something like LLVM but for databases.
As for the NoSQL, I think it was the worse thing that happened to databases in the last 20 years, probably more
Infuriating as it is, this is still better than with the bad old days of taxis, which usually had even worse resolution and accountability. It sounds like people don't quite grasp just how bad the taxi experience was.
To be clear the happy path for taxis for me was fine. When things worked things were quite smooth. But this thread is primarily about when things went off the happy path. If a taxi didn't show up, I'd usually have a disinterested dispatcher to talk with who might be able to send another in a half hour. If a taxi intentionally went the long way around to charge more, I'd have to have an argument with the cabbie about this and maybe things would go well maybe they wouldn't. While I didn't personally experience harassment from cabbies I definitely know people who have. So on and so forth. In all of these cases off the happy path the usual recourse back then was worse than the recourse today with e.g. Uber.
Again the overwhelming majority of my taxi rides were fine. The overwhelming majority of my Uber rides are also fine. But when things go wrong they definitely went wrong worse with taxis than Uber rides for me.
I can share an example of a trip we just did to South America to two countries. Four out of four taxi rides were scams. Things are better to the extent there were controls in place, like taxi meters and an app. There the scam was less but still involved scams. Too long to detail in a comment here.
I should also mention we tried to use their version of Uber (DiDi), but I suspect there was some kind of price-fixing attempt there because no taxis would come for the price that they suggested. We had the option of upping our price until someone came and then I gave up on the service.
My other experiences were some years back in upstate New York, where there were also questionable practices, and you really had to look over the driver’s shoulder. They tried to control scams with payments based on zones, and the drivers would bend the rules when possible.
> For some programs, the shortest descriptions of what they do are the programs themselves.
There is almost no real-world program for which this is true. One corollary of this would be that it is impossible to refactor the program to be any cleaner, which is not true for basically any large real-world program.
Another corollary of this is that no observable aspect of a program could be changed without breaking user expectations, but this too is almost always wrong (e.g. almost always, but not 100% via e.g. the famous xkcd comic about spacebar heating, a global performance optimization would be viewed as good).
You could imagine the typechecker has bugs (and indeed another comment mentions examples of bugs!). Crucially though anytime the typechecker has a bug fixed you could rerun the typechecker on the code to see if it still type checks.
This is the whole promise of formal verification. It reduces the problem of verification purely to the typechecker. If the typechecker is correct, then the proof is verified, no matter how many lines of code the proof is. As a sibling comment puts it, the chance of bugs mainly scales with the number of lines of code in the typechecker, not in the amount of lines of Lean code.
Your question is akin to asking, "yes this spellchecker ran fine on your essay, but are you sure it runs fine on War and Peace? That's 1000x more words!" To which the answer is the number of words doesn't matter if the spell checker is correct (which it might not be! And longer passages might reveal more bugs! But you can always rerun it). The main source of bugs is more lines of code in the spell checker, not in number of words in the text.
reply