Bingo. Local cop goes in, buddy-buddys with the loss prevention manager, gets access to run plates for the immigration folks outside. "Professional courtesy" strikes again!
Thats not the point, if there were a better proprietary engine stockfish would still be there as a baseline. Anyone can access an engine as good as stockfish to practice against. Are any open models touting mathematical breakthroughs?
There is money in this, so of course the closed models are far ahead. The open models will likely catch up a bit at some point, just as Stockfish caught up to AlphaZero. That being said, there are already a couple. It seems Deepseek has a claimed proof to the "Ziegler's Cross-Polytope Conjecture" [0], but I can't speak to the significance of the result.
It would be nice if OP noted what caused the change in their opinion?
did datafusion gain some feature that they noted was missing in the previous article, or did something in their understanding click so they could overcome the previous issues?
The previous issues were in my mind, not in DataFusion.
I tried using DataFusion as an in-memory tool, which was a mistake. If the graph fits in memory, Networkit, IGraph, etc. will almost always be faster. These tools cannot process anything bigger than the available memory.
So, I changed my approach. I wrote my own naive "disk checkpointer," offloading everything to disk and avoiding materialization. Although I was afraid that writing to and reading from the disk would be slow, it is surprisingly fast with DataFusion. The results are impressive: fast and out-of-core.
Sorry, this post is short and not very detailed. I did not expect it to be at the top of HN and receive so much attention.
I thought of datafusion work and the rust implementation as a way to address the delta seen vs the Spark/JVM GraphFrames implementation (author is a major contributor).
Looking forward to more such innovations, which will benefit the ecosystem as a whole. Why would anyone want to use a pure python graph algorithm package unless they're dealing with toy graphs?
We shared with the author how databricks multi-node and single-node graphframes were wildly inefficient for this kind of thing: we were measuring doing billion-edge graph traversals & scans in single node in-memory in seconds with regular dataframe (cudf) libraries, so the core of pagerank, which is magnitudes more efficient than their original spark approach
So then the question became pandas/polars/datafusion/duckdb/etc, must of which are rust/native. I'm curious myself why datafusion vs others, it's an interesting project :)
All "dynamic" means is that you don't know or don't prove the precise value statically. However you may know the range of possible values, or you may know properties of your algorithm that mean it can never attempt an out-of-bounds access. Sometimes you don't know any of these things, but sometimes you do.
What I was (badly) trying to express was more that given static bounds rust could also eliminate dynamic checks. So saying e.g. ATS can eliminate static checks, is kind of switching the target.
I'd also say a few things, if knitting takes a long time consider how long it takes to make a good clear pattern so that others can replicate it.
People who make patterns are already dealing with a saturated market.
This includes historical/vintage patterns, which for many years patterns were primarily given away freely to incentivize yarn sales, or dominated by publishers. It wasn't until recently (internet, etsy, ravelry) when designers actually had the means to sell directly to consumers. People making an effort to produce usable patterns are now being dwarfed by AI nonsense in the speed of their output. It was already a difficult market. That everybodys images of real objects (along with AI generated ones) are being used to peddle and market patterns that will never work can be really demotivating.
One last thing is how many of the 8 people in this podcast company are actually generating slop and how many are actually just doing marketing?
If you only care about the material and physical utility of the product, you can order the sweater from AliExpress for 5% of the cost and no time spent.
The same way that the AI generated podcast about knitting, or engaging in consumption is enjoyable for many people and a form of stress relief, which was the point that the comment above was criticizing.
So the conclusion is that the utility of the activity is subjective, and if most people spend their time listening to AI factually incorrect podcasts about knitting and enjoying it, it's no different than knitting yourself and enjoying it. The blog was poor in this disambiguation, and pushed a more Aristotole-like ontological view of what is meaningful, which is more common view in engineering/hard-science dominated fields.
They are not the same. One is a passive thing (viewing) and the other is active (physical creation). We should not mistake one for the other. It is like the difference between listening to music and making it.
It is fine though if people who don't knit enjoy knitting podcasts, but this is not that. Somewhere between the producer/consumer relationship there should exist some actual knitting. Otherwise (in cases like this) it's just plain exploitation.
That's completely your subjective opinion that ignores reality. If people feel like they are participating in something, or they feel like their identity is based on something they consume passively, it's as valid as the physical thing.
If people did not feel good from passive consumption, no-one would be listening, following or looking at things, people would just make and create all the time, which is obviously not true.
If what you say is true, there would be no value from AI-generating blogs in question, or AI-generated movies/youtube films. Yet both have millions of downloads, views and listens, as the article mentions.
Reality involves physical objects you can hold in your hands, not abstract experiences. Abstract experiences are subjective not objective most of the time.
Knitting is not just entertainment, it's a means to produce useful things as well as artistic projects.
Many people are either lazy or have been discouraged from creativity by a consumer society and the education system. I've watched plenty of online content. I have nothing from it but feelings (the very subjective opinion you talk about), and very occasionally a tiny bit of new information. Knitting creates clothing which can be used to keep out the cold (objective) and so on. In fact this very winter, I wore things my friends knitted me. Gloves, hat, socks, snood, scarves... They served a practical function beyond entertainment or just looking good.
Seriously? You can't get the feeling of satisfaction of wearing something, or having someone wear something you made from AliExpress. My point is your sense of feeling and validation is extremely distorted if you have no knitted material to show for it?
Completely subjective take by you with similar epistemology around value as the blog author.
People might not care. I might identify as a runner because I bought a little jacket, expensive shoes, and wide-purple-tinted sunglasses, do I have to run? Not necessarily if the objects and my identity gives me the feeling of completion and satisfaction.
If your premise was true for all people, and the sense would be distorted, we would not see these phenomena, and people wouldn't listen or engage with AI-content. But the biological reality and the path of least resistance seems to prove us otherwise.
My only complaint with the article is that it doesn't seem to mention that digitized proofs can contain gaps but that those gaps must be explicit like in lean the `sorry` function, or axioms.
Carr made public comments January 29.[1] The 1st news report of FCC investigation was published February 7 seemingly.[2] And CBS's risk and reward estimates for a current official and a candidate could have differed.[3] And Ossoff and Shapiro had not filed as candidates reportedly.[4]
why do we invent these formal languages except to be more semantically precise than natural language? What does one gain besides familiarity by translation back into a more ambiguous language?
Mis-defining concepts can be extremely subtle, if you look at the allsome quantifier
https://dwheeler.com/essays/allsome.html you'll see that these problems predate AI, and I struggle to see how natural language is going to help in cases like the "All martians" case where the confusion may be over whether martians exist or not. Something relatively implicit.
We build pretty complex systems only based on "natural language" specifications. I think you are conflating specification ambiguity with verification accessibility.
> What does one gain besides familiarity by translation back into a more ambiguous language?
You gain intent verification. Formal languages are precise about implementation, but they are often opaque about intent. A formal specification can be "precisely wrong". E.g. you can write a perfectly precise Event-B spec that says "When the pedestrian button is pressed, the traffic light turns Green for cars"; the formalism is unambiguous, the logic is sound, the proof holds, but the intent is fatally flawed. Translating this back to natural language ("The system ensures that pressing the button turns the car light green") allows a human to instantly spot the error.
> All Martians are green
Modern LLMs are actually excellent at explicating these edge cases during back-translation if prompted correctly. If the formal spec allows vacuous truth, the back-translation agent can be instructed to explicitly flag existential assumptions. E.g. "For every Martian (assuming at least one exists), the color is Green", or "If there are no Martians, this rule is automatically satisfied". You are not translating back to casual speech; you are translating back to structured, explicit natural language that highlights exactly these kinds of edge cases.
Maybe it can be done, but I struggle to believe adding in that branch for every forall quantifier (which may be plentiful in a proof) is going to help make a proof more understandable. Rather I feel like it'll just balloon the number of words necessary to explain the proof. Feels like it's going to fall on the bad side of verbosity as the sibling comment said.
I think there is a misunderstanding about what is being back-translated.
We don't back-translate the proof steps (the thousands of intermediate logical derivations). That would indeed be verbose and useless.
We back-translate the specification: the Invariants, Guards, and Events.
For a traffic light system, we don't need the LLM to explain the 50 steps of predicate logic that prove inv3 holds. We just need it to translate inv3 itself:
Formal: inv3: light_NS = Green ⇒ light_EW = Red
Back-translation: 'Invariant: If the North-South light is Green, the East-West light MUST be Red.'
This isn't verbose; it's the exact concise summary of the system's safety rules. The 'verbosity' of handling edge cases (like the 'Allsome' example) only applies when the specification itself relies on subtle edge cases, in which case, being verbose is exactly what you want to prevent a hidden bug.
Definitions are built up layer upon layer like an onion too, with each step adding it's own invariants reducing the problem space.
I just feel like the street light example is an extremely small free standing example. Most things that I feel are worth the effort of proving end up huge. Forever formal verification languages were denigrated for being overly rigid and too verbose. I feel like translations into natural language can only increase that if they are accurate.
One thing I wish is this whole discussion was less intertwined with AI.
The semantic gap has existed before AI, and will be run into again without AI.
People have been accidentally proving the wrong thing true or false forever and will never stop with our without AI help.
At the very least we can agree that the problem exists, and while i'm skeptical of natural language as being anything but the problem we ran away from. At least you're trying something and exploring the problem space and that can only be cheered.
My bet is that AI changes the economics of that verbosity, making it cheap to generate and check those 'huge' definitions layer by layer. The next four years will show.
I agree, if AI (or humans) have mistranslated a natural language statement to a formal statement, we should not rely on AI to correctly translate the formal statement back into natural language.
For many statements I expect it's not possible to retain the exact meaning of the formal-language sentence without the natural language becoming at least as complex, and if you don't retain meaning exactly then you're vulnerable to the kind of thing the article warns about.
> if AI (or humans) have mistranslated a natural language statement to a formal statement, we should not rely on AI to correctly translate the formal statement back into natural language.
Perhaps we must not rely on it and find a way to make sure that it cannot fail, but I like to point out that this are two different problems and it seems to me that the current crop of so called AIs are pretty good at distilling excerpts. Perhaps that's the easier problem to solve?
> why do we invent these formal languages except to be more semantically precise than natural language
To be... more precise?
On a more serious note, cannot recommend enough "Exactly: How Precision Engineers Created the Modern World" by Winchester. While the book talks mostly about the precision in mechanical engineering, it made me appreciate _precision_ itself to a greater degree.
Rhetorical sentence? My point is that back-translation into natural langauge is translating into a less precise form. How is that going to help? No number of additional abstraction layers are going to solve human confusion.
> Proprietary use, commercial redistribution, or publishing modified versions with ads or tracking is strictly prohibited under GPLv3 or later.
These all sound to me like "Further restrictions" which the GPL says:
> If the Program as you received it, or any part of it, contains a notice stating that it is governed by this License along with a term that is a further restriction, you may remove that term.
It seems like if you want those clauses that GPL doesn't seem like the license you want?
The reason I included that note is that, as an open-source developer, I’ve seen many projects that weren’t actively maintained get picked up by bad actors as they modify the code and publish it on Google Play with ads or IAPs. I wanted to discourage that.
Other than this notice, MBCompass is fully licensed under GPLv3 or later.
The sum of the note and the gpl doesn't behave as though the notice has any precedence over the gpl. It behaves as additional restrictions and a license that allows you to ignore the additional restrictions. I'm no lawyer but it seems like it isn't achieving what you want.
> I’m planning a non-intrusive in-app prompt to remind users about donations something subtle, because many users forget once they start using the app, rather than only seeing the donation info in the README.
As I mentioned previously, the above approach seems to be well enough and good.
That sounds very weasel worded, if they get license plate readers from someone who does.