If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does something other than what you intended. This is one of the harder parts of verification: clearly expressing your intention as a human. As programs get more complex these get harder to write, which means it isn’t uncommon to have lean or rocq proofs for everything only to later find “nope, it has a bug that ultimately traces back to a subtle specification defect.” Once you’ve gone through this a few times you quickly realize that tools like lean and rocq are tricky to use effectively.

I kinda worry that the “proof assistants will fix ai correctness” will lead to a false sense of assurance if the specs that capture human intention don’t get scrutinized closely. Otherwise we’ll likely have lots of proofs for code that isn’t the code the humans actually intended due to spec flaws.

A recent example for me: I had a challenging problem in a medium sized codebase (tens of thousands of lines) that boiled down to performing some updates to a complex data structure where the updates needed to be constrained by some properties of the overall structure to maintain invariants. Maintaining the invariants while the data structure was being updated is tricky since naive approaches would required repeated traversals of the whole structure. That would be really inefficient, and a smarter approach would try to localize the work during the updates. The latest Claude and GPT assistants recognized this, but their solutions were exceptionally complex and brittle. I eventually solved it myself with a significantly simpler and more robust method (both AIs even gleefully agreed that my solution was slick after I did it).

Had I let my CS fundamentals go to waste I wouldn’t have been able to solve it myself, nor would I have been able to recognize that the solutions posed by the models were needlessly complex.

Just because an AI can generate a solution that passes tests quickly doesn't mean what it generated is a long term good solution. Your skills in fundamentals is key to recognizing when it does a good job and when it doesn’t, and being able to guide it in the right direction.

“The influencers presented their claims as exposés of industry deceit, despite offering no verifiable evidence to support them.”

So, misinformation = make claim with no supporting, verifiable evidence. Seems like a pretty standard, neutral definition.

I don't think the post implied that this package writing activity was a write-only activity where reading and learning is strictly forbidden.

> You can find open source licensed packages, read them to understand them, and then copy them into your config. Doing everything from scratch is a waste of time unless you enjoy the process (in which case go nuts).

The post clearly indicates the relatively large set of open source packages they looked at and understood before doing their own packages. The author graciously acknowledges them and their influence on the work:

"Emacs Solo doesn't install external packages, it is deeply influenced by them. diff-hl, ace-window, olivetti, doom-modeline, exec-path-from-shell, eldoc-box, rainbow-delimiters, sudo-edit, and many others showed me what was possible and set the bar for what a good Emacs experience looks like. Where specific credit is due, it's noted in the source code itself."

Woxi reminds me of some experiments I did to see how far vibe coding could get me on similar math and symbolic reasoning tools. It seems like unless you explicitly and very actively force a design with a small core, the models tend towards building out a lot of complex, hard-coded logic that ultimately is hard to tune, maintain, or reason about in terms of correctness.

Interesting exercise with woxi in terms of what vibe coding can produce. Not sure about the WL implementation though.

(For context, I write compiler/interpreter tools for a living - have been for a couple decades)

So, yeah. They just made it up because it felt right. (Which, I guess is what one would expect from AI related stuff these days.)

You’re definitely right though: it doesn’t take a deep dive into the history of computing and programming languages to find higher-than-assembly level languages emerging at the very dawn of computing.

This I can’t relate to. For me it’s “the better I build, the better”. Building poor code fast isn’t good: it’s just creating debt to deal with in the future, or admitting I’ll toss out the quickly built thing since it won’t have longevity. When quality comes into play (not just “passed the tests”, but is something maintainable, extensible, etc), it’s hard to not employ the Thinker side along with the Builder. They aren’t necessarily mutually exclusive.

Then again, I work on things that are expected to last quite a while and aren’t disposable MVPs or side projects. I suppose if you don’t have that longevity mindset it’s easy to slip into Build-not-Think mode.

Perhaps if we didn’t have deep layer cakes of frameworks and libraries, people would feel like they can code with or without AI. Feels like AI is going to hinder any efforts to address complexity and justify us living with unnecessary complexity simply because a machine can write the complex, hard to understand, brittle code for us.