Paracompact

[flagged]

Very confidently wrong.

Do you know why it's easier to specify theorems than it is their proofs? Or why ACSL != C?

You can go ahead and make a more specific argument, e.g. that mainstream UX-centric software development may not be amenable to current paradigms of formal verification, but to insinuate that a complete spec reduces to source code itself is naive.

EDIT: Possibly I have responded too acutely to the points you care less about. I agree that "in the future we won't need programmers" is questionable since good spec-writing and spec-vetting requires at least as much expertise, if not more, than ordinary coding work, and that is fair to call comprehensive spec work "code" in that it is technical and formal. But it is decisively not source code.

Thank you. As far as circumstantial evidence goes, yours is more intriguing and cause for inquiry.

> According to the petition, two people asked [Meta AI] to pick a number between 1 and 25. They gave no instructions and made no reference to the election. In one attempt, the AI answered 13. In the other, it answered 22. Those are the party ballot numbers of Lula and Flávio Bolsonaro, respectively. The groups question the coincidence.

My confidence in the validity of their claims tanked right about here.

I'm all for regulating transparency into social media algorithms. Meta most certainly is compromised by foreign actors. But can we choose less stupid hills to die on than numerology and GIFs? Headline is not remotely supported by the evidence.

> This is exactly why we use code... Natural language is ambiguous, to a fault. Any statement can impact depending statements in multiple ways, which creates this huge dependency graph that has millions, billions, trillions of "plausible" specifications.

Devil's advocate here: Why is having many possible implementations a bad thing? Sure, you don't want to half-ass your specifications and fail to pin down your product properly, but if you do pin down what matters, then by definition what remains is discretionary. Formal specs (e.g. the C spec) behave the same as informal specs in this regard.

The real question is whether humans in an agentic workflow can actually identify all of what's structurally and functionally necessary for their product. Either the spec writer must be expert, or the agent must be savvy enough to identify and collaborate with the non-expert. Right now, agents like to just plough through underspecification or bad ideas so that they can deliver as quickly as possible.

The blog post mentions rising standards of quality enabled by AI-assisted code review, and that reverted code predates the era of AI. Even very competently managed codebases are not above mistakes, especially when held to as high of a standard as this.

> What differentiates them from any other spam bots or people out there submitting junk to random POST endpoints?

Hacking websites and submitting false police reports.

The amount of time and effort a human put into something very much does tend to determine its value, both to that human and others in their social circle.

> Make a three.js (pnpm) visualization of all Invisible Cities by Italo Calvino. Don’t ask questions, it is a one-shot task. You have 6h of work, use it until it becomes a masterpiece.

I am an expert (in formal methods). LLMs absolutely need more safeguards rather than less. Not because they /need/ them in order to produce functioning code, or even because they produce as many braindead bugs as humans, but because in an era of explosive code quantity, what has become valuable is (assured) code quality.

Going back to C++ would be particularly bizarre to me given that AI is also very proficient at verified languages. Not merely typesafe, but languages comprising their own spec languages such as Rocq and Lean.

I predict that in the next decade: (1) the market will understand the difference between a "code writer" and a "spec writer," with (2) the expectation that the latter is overwhelmingly more necessary than the former in an AI-dominated field, and (3) there will emerge more useful and less mathematically specialized formal verification alternatives to Rocq and Lean, and a filling-out of the tooling gap of between "static typing" and "interactive proof assistant," perhaps in the vein of ACSL-like contract annotations, and (4) there will be a subsequent shift in the traditional curriculum for programmers. Since educational change is slow (and spec writing depends on good coding fundamentals anyway), perhaps (4) is a stretch, but I'm more confident in the first three.

> They have more of an obligation to make money for their investors than they do anything else, that's just how it works

Where does this myth come from, and how does it survive? It's either an excuse for parasitic corporatism, or an expression of learned helplessness. Nobody has been successfully sued for prioritizing the long-term health and reputation of a company over self-starving quarterly profit.

Is there a perverse incentive toward the latter anyway? Yes. But it mostly serves current leadership, who are evaluated and paid on short horizons, at the expense of the long-term investors who own most of the equity.

A model of lambda calculus with a much smaller Kolmogorov complexity, then.

Elon's mother recently posted an AI-generated photo of her son's birthday party. The tag indicating such was scrubbed as soon as it was pointed out.

> Anyone who is even quite intelligent but has really pursued the rigorous stuff, unless they are in fact a prodigy, eventually realizes they have an abstraction ceiling

Eh. I'm a math PhD who fled academia because it was too much for me. But I have never encountered this term "abstraction ceiling" nor did I succumb to it. I simply ran out of motivation to pursue higher math, especially when following through on learning and research became more and more labor. (It was always labor; but it was a labor I used to love.) I am far from a prodigy.

> even epsilon-delta proofs are enough to eliminate the majority of the population, no matter how good a teacher you are

Disagree. It's a notoriously hard subject to teach, and with all the demands placed on e-d in so little time in your average curriculum, it doesn't require appeals to IQ to explain its infamy. With enough motivation and practice, the quantifier alternation is comprehensible to any sound mind. What your average mind (and student) lacks is exposure to formalism, abstraction, and how these things tie in with what they are familiar with, which is symbolic manipulation. With the exception of geometric proofs (another educational bugbear), they have little context for what formalism is or why it matters.

Another response to math that makes me sad: "I must be too stupid to understand this," "my brain is too small for this," etc. Different people say it for different reasons, but it's almost always in response to a hand-wavey explanation that doesn't makes sense to anyone not already in the know. Math is so much more about humility and skepticism than it is prodigy.