> Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible.

This is so reductive a framing as to be essentially useless [0]. I think maybe you want to learn more about program correctness, formal verification, and programming language semantics before you make such statements in the future.

[0] See, e.g., type-checking.

And Alonzo Church proved in 1940 that you can avoid this problem by using a typed language in which all programs halt. But sadly some programmers still resist this.

Some correct programs are supposed to run forever.

When is an OS supposed to halt? When you shut it down, or when you power down the hardware, and no other times. So if you don't do either of those things, then the OS is supposed to run forever. Does that, by itself, mean that the program is incorrect, or that the language is inadequate? No, it means that the definition is worthless (or at least worthless for programs like OSes).

you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.

> finite programs that run on an infinite stream of events

This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.

Two different meanings of "forever" there. An OS runs for an arbitrarily large finite time, which is different from an infinite time.

Same way you can count to any finite integer with enough time, but you can never count to infinity.

Those kinds of interactive programs take in a stream of input events, which can be arbitrarily long, but eventually ends when the computer is shut down.

Termination checkers don't stop you from writing these interactive loops, they only stop non-interactive loops

This is not actually a problem for total languages, which simply model these kinds of processes using corecursion/coinduction/codata.

When you write a recursive function, Lean’s kernel requires a termination proof, unless the function is a partial or marked as unsafe. In those cases, they can’t be used in proofs. https://lean-lang.org/doc/reference/latest/Definitions/Recur...

> reasoning about program correctness is not possible

Not possible for all problems. We cannot decide correctness (ie adherence to a specification) for all programs, but we can definitely recognize a good chunk of cases (both positive and negative) that are useful.

The Halting Problem itself is recognizable. The surprising result of Turing’s work was that we can’t decide it.

We care only about a very small and narrow subset of possible programs, not any arbitrary one. It's possible to solve this kind of problem in large enough classes of program to be useful.

> a given arbitrary program and input

Keyword emphasis mine.

That one little word that changes everything in how you interpret the statement.

A decent JSON formatter should really ship natively in the browser as well.

Agreed. Firefox ships with one, and it's very useful.

I bet Satya Nadella is regretting defending Altman now.

satya defending altman is more like satya want to save his own ass

They can just file another DMCA against Codeberg, what am I missing here?

Sounds like Codeberg would still take down the repo, but would be more supportive: https://blog.codeberg.org/on-the-youtube-dl-dmca-takedown.ht... (2020)

Maybe there are more recent examples?

For real. Use https://radicle.xyz/ if you want actual takedown resistance.

Or self-host Forgejo?

This is what the Eden switch emulator does ever since Nintendo went after them on GitHub.

That won't be easy because Codeberg follows German law.

And German law is more restrictive than U.S. copyright law, with fewer protections for content uploaders and service providers. There is also no concept of fair use that limits copyright.

I want Codeberg to succeed, but running an open code hosting platform (both in the sense that anyone can create an account, and the service source code is publicly available) in the European Union, and especially Germany, is extremely challenging from a legal perspective. Sadly, once they become successful and popular, they will have to implement all kinds of weird stuff, like proprietary scanners for potentially infringing content prior to publishing it.

Germany and the EU will probably kowtow to the US if the DMCA requests or lawsuits are brought by big enough players.

Big money interests rub shoulders with US politicians, US politicians deal with their overseas counterparts. Therefore, big enough DMCA requests will be mentioned behind closed doors in the same breath as international trade and other geopolitical concerns. Money protects money in deals between close enough friends and allies.

If Codeberg were based in Russia or a US geopolitical adversary, on the other hand, such requests would likely be ignored.

A DMCA takedown is targeted at the host and is a pre-lawsuit thing ("we claim X and if you take it down now your host is safe" via the DMCA Safe Harbor provisions). If they escalate to lawsuits then not sure it's significantly different in Germany vs the USA. It's not like Europe is free from things like blocking all of Cloudflare because the football league wants to.

This procedure only applies to copyright-infringing content, not to trafficking in circumvention devices. It seems that in this case, it's the latter.

Just ChatGPT? Or are the rest also just as capable at delusioning users?

I'm very confused because there are 2 Andrews, the author in the blog post only states "Andrew", and by the list of Authors the author seems to be Andrew Gelman, but the slug in the first link is "aking", and then there is also Andrew King, lol.

Andrew King seems to be the person who published the original exposé of the paper:

> The above story came from my occasional collaborator Andy King [...]

> the author in the blog post only states "Andrew"

If you click on that "Andrew", it takes you to [0] which is clear that it's Gelman.

[0] https://sites.stat.columbia.edu/gelman/

One wonders why this sort of research isn’t in academia but in startups instead.

Where in academia can one get a Billion (with a b) dollars to research something?

I’m an early fan (Polymer, anyone?) but somehow the mindshare is just not there and trying to evangelize it to mainstream was too much. So now it just kinda there for people to slowly discover when they run into niche use cases.

404