He doesn't need one. This is ridiculous, and you're being ridiculous.

AI is here, and it's not going anywhere. It's not going to be pretty, but the people that are going to be hit the hardest are those who cannot -- or worse, refuse to -- adapt.

I'm sympathetic -- I feel both a loss and an existential dread. I've also never, in my 30 years in my field, seen something sweep the technology space so quickly and change things so much overnight, and I see no chance of it stopping anytime soon.

Perhaps LLMs change that calculation. I really couldn’t say.

The problem has always been:

- It's extremely labour-intensive, and even small changes to the code can require an enormous amount of new proof work.

- The skills required to formally verify software are very different from the skills required to write it, and the set of people capable of doing so is much smaller.

- Code has to be written with verification in mind, against a specification that expresses invariants that can actually be verified, and that is coherent enough that you can derive useful high-level properties of the system from it.

You needed two teams — verification and development. Verification would always be behind the development team, while also having to feed requirements and design changes back to the developers. Everything slowed to a crawl.

AI changes this. A coherent, verifiable, useful specification isn't easy to write — but it's far easier to write than the software itself, and AI can do most of that work: both drafting the spec and proving that it's consistent and that the high-level properties you actually care about follow from it.

More importantly, a high-level spec is far easier to read and reason about than the reams of code required to actually implement something. Which means:

- AI does the grunt work of writing and proving the spec; humans only have to carefully review that high-level artifact.

- AI writes code it must also prove conforms to the spec, so humans can be assured it's correct without babysitting the AI.

- Changes are driven top-down: evolve the spec first, then have the AI fix the implementation and re-prove conformance.

Our (very, very large) company is rapidly going all-in on formal verification across projects we never would have dreamed of verifying before; the velocity hit and the man-hour cost were only worth paying for truly critical infrastructure.

The books aren’t banned.

Declining to provide a book is not the same as prohibiting the possession, use, or distribution of a book.

As for “external parties”, schools in the US are public institutions.

The book can still be printed, bought, and read. It can be brought into that same school, and read there. It’s not banned.

And it was first hosted at OpenDarwin — which was Apple-run and not available for arbitrary public hosting.

It was then hosted at OpenDarwin’s successor — Mac OS Forge. That was also Apple-run and not available for arbitrary project hosting.

MacPorts was an Apple-authored and ultimately Apple-supported project for ~15 years.

As for momentum, the project is still going strong 25 years later, so I’m not really sure what you’re referring to.

The final straw was when we had to hire a fixer to clear up a state regulatory error that would’ve destroyed our business. No amount of calls or letters over months — by me — fixed the issue. The guy we hired got it cleared up in a week.

That’s how I learned firsthand that the more involved the state tries to be in protecting everyone from everything, the more opportunity there is for bad actors and gross inefficiency, and the worse things get.

I would strongly reconsider pivoting unless you actually want to work for no-name companies and on the shady side of technology for at least the next decade.

This is in direct violation of the terms of service, and Apple invests a lot of money in keeping iMessage clean of this kind of misuse.

They control the servers, the client, certificate provisioning, hardware identification, and user identification. They can trivially trace a registered account to the point of sale and the card and PII used to buy the hardware on which the account was registered.

You will fly under the radar for just as long as it takes to annoy enough of their customers that Apple brings down a massive ban hammer.