Paracompact

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.

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.

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.

Hacking websites and submitting false police reports.

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.

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.

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.

Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.

The fear is not that they will just slow down progress for all. It is that regulation will specifically burden competition. If you kill open-source training, ban Chinese models, crack down on self-hosting, grandfather OpenAI/Anthropic/Google into regulatory compliance while throwing the book at startups, etc. you wind up in the worst of all possible worlds.

At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.

Do you believe no open questions remain as to the truth of the Collatz conjecture?

Second of all, you did not read the link.

> In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC).

Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.

After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.

It's objectively very difficult and technical, it's spatiovisual, it's artistic, learning resources for it are sparse and most just learn by the FAFO method, current AI sucks terribly at it, and it's not likely to ever be specifically targeted by benchmaxxers.

I was using an AI to help me set up a container to be used as the Nix build environment for another AI. This build environment would not have Internet access. I was having it base its approach off a previous container used for a Stack build environment.

In its initial analysis of my proposed strategy, it insists as its premier point /against/ the strategy, "you will have to rebuild the container every time your flake.nix changes."

Two head-slapping errors of judgement in saying something like that:

(1) The Stack solution is identical. Change stack.yaml, the container must rebuild. (2) It is not physically possible to do better than this while insisting on an internet-free environment.

So on this point, it was just parroting advice irrelevant to the context at hand. LLMs always have such a bizarre mix of technical knowledge and lack of good judgment.