This article mentions a few of the reasons why some of our best attempts at defining languages that are "trivially correct" keep failing.

Among other examples, it specifically mentions that you if lego together two Push-Down Automata chatting with each other you get a Turing Machine back out. It doesn't include my other favorite recent example that we found a 0-day sandbox escape in the Universal Turing Machine itself.

The problems generally keep coming back to the Church-Turing Hypothesis that if you've got one Turing Complete language you've got theoretical access to them all.

Turing Completeness in turn seems an "emergent property" rather than a hard bar to clear. Rule 110 [0] shows Turing Completeness in the mathematical equivalent of a petri dish. We've built Turing Machines out of Magic the Gathering card game decks [1].

To some extent if there was a way to build a truly, well enforced, secure scripting language you would think that we would have already found it given how important it would be to security and to safety.

[0] https://en.wikipedia.org/wiki/Rule_110

[1] https://www.toothycat.net/~hologram/Turing/index.html

But again, I don't need the full Turing complete machine. I can just say something like no function can have more than 1000 calls in a fun, and similar for loops - that's suddenly going to take away a lot of your Turing machine.

I'm not sure where the limits we need to place are, but that's the reasonable place to start.

The author of this article goes into the academic details on "Total languages" (under the headline "Limiting our scope") because they have been explored before. A specifically useful quote:

> The restriction made by total languages, therefore, does not help make verification any easier. Indeed, it would have been surprising to discover that an impossible problem becomes easy by restricting it just a bit (giving up leather seats does not reduce the cost of a car by 90%). We also note that every program could be trivially made total by adding a large counter, say 2^100 to all loops – this won’t change its physical semantics in any way – so we can already assume all real-world programs to be written in total languages without loss of generality. If total languages helped, we could have assumed all languages are total.

To rephrase it a little: all of our Turing Machines are limited (by RAM, by power, by transistor count, etc) compared to the Universal Turing Machine (infinite in scope, as a thought exercise), but that doesn't make solving safety or security easier.

If no one function can have 1000 calls, you make a million functions. If no one loop can go more than 1000 ticks, you put that in a function and call that function in a loop. Suddenly you have access to a million iterations through a loop.

The problem with Turing Machines is that even (intentionally) broken ones always tend to have unexpected sandbox escapes.

It's the same boolean value that you are testing: does it "halt" because it completed its computation successfully or does it "halt" because it failed? If Program A terminates on success and Program B terminates on failure you can generally rewrite one to be the other (run Program A in a busy loop after a success; monitor Program B in another process and report the first success then kill B). Ultimately, you have the same decidability problem asking "does it halt?" and if you could solve it for one case you could solve it for the other.

In fact, it's generally considered a harder problem to include the second boolean "does it halt successfully?" Does it stop at all is a hard enough question before asking if it stops with a success or a failure/crash. In practice this is often the easier problem to debug: once it stops we generally know if it was successful or failed. But that doesn't help to answer the questions like "will it always stop successfully?" or "will it 'forever' run successfully without ever stopping for a failure/crash/hang/deadlock?"

Just as LAN addresses (link local) are usually 192.168.$x.$y and you are just passing $x.$y, with IPv6 they are usually `fe80::$z` and in theory you could just pass $z and the person on the other end can assume `fe80::`. Because of how double colon works $z could be just 54 in a similar situation (especially if link local addresses are statically assigned like most workplaces try to statically assign IPv4 addresses).

Same with ULA addresses like 10.$x.$y.$z for private networks. Most of those you can assume `fd$x::$z` and just need to pass whatever is on the other side of the double colons. (Where $x is optional and likely network-wide.)

They're long though. Just checked and my desktop has fe80::1068:f88b:8b1b:4e45 for en0. They can't be short because of possible collisions, unless you're using DHCP or manually allocating static ones, and DHCP6 isn't broadly supported on hosts or routers.

Sure, most systems default to SLAAC which creates random long addresses. You can manually allocate them just fine and short addresses aren't going to cause collisions (and if they did, SLAAC handles it). Some of the networking people most (ab)using 192.168.x.y heavily are manually allocating them.

DHCP6 is pretty well supported on a lot of Enterprise routers, so the fd:: ULA space, which is what DHCP6 is most good for, has no required reason to be long addresses (outside of silly things like this link's mentioned Tailscale fingerprinting/advertising IP).

mDNS already serves homelab.local style addresses.

Also, link local is almost always `fe80::` [0]. Today for privacy (and simplicity) reasons most devices pick a random address under that like `fe80::6923:83ab:201:273e`. But most operating systems allow configuring a static link address so if you really wanted you could use `fe80::403e:7ab` for something close to "homelab" (and `fe80::cafe` for your coffee maker) you absolutely can.

[0] The allocated range is fe80::/10 so fe(8|9|A|B)[0-F], but in practice it seems rare for devices today to use anything but fe80::.

Of course Congress risks a potential Constitutional Crisis in that mandate. The USPS is one of the only services of the federal government that is Constitutionally mandated. The contradiction of Congress wanting USPS to act as if it were a for profit business remains an interesting balancing act versus the Constitution.

(It's also not a surprise that the Congressional mandate to run the USPS as a for-profit has been used as much to make the USPS profits a slush fund of "free money" that Congress can use for non-USPS projects, including pork barrel projects. The for-profit mandate isn't just for threatening the shutdown of USPS services.)

It's probably a horror story if we ever find out.

Given its prominence in some of these other discussions from GitHub of a repo always on their performance radar now my gut instinct is that it could be the Windows monorepo.

The anti-trust laws are still on the books even though they aren't currently being enforced effectively. It's not congress that needs to act right now, it's the executive branch that needs to execute the laws (by making judicial cases out of it, proving that laws were broken in the right courts). Which means getting a President and staff (FCC, FTC, SEC, and especially Attorneys General staff) that cares about these things, and having healthy competition in the market.

It's a reminder that Congress is intentionally only one piece in the three part puzzle and you can't just put all your hopes in the basket of a single Congressional midterms sweep, you also still need the other two branches functioning well. It's also a reminder that the DOGE cuts destabilized a ton of executive branch staff that may take decades to repair. The new historically weak FTC and FCC lost a lot of power to preempt anti-trust behaviors, putting more strain on after-the-fact/after-the-damage enforcement that requires the Executive and Judicial branches working together versus simpler Executive branch only "preventative defense" outcomes.

Enforcement is part of the problem, but the other problem is judges. The 'consumer welfare' doctrine of anti-trust has in large part served to justify not breaking up companies that really should be broken up.

Judges are part of enforcement, not an orthogonal concern. (And judges are appointed by the executive branch based on its priorities, so a long term trend of executive hostility to effective antitrust is likely to be reflected in the judiciary as well.)

Microsoft has already had execs saying the next big thing is AI rewriting stuff to Rust. You think you are joking, but I'm sure it is on someone's roadmap in the Teams org.

Of course, being the Teams org they'd likely still find a way to end up with a bloated mess even after a Rust rewrite.

Page response might be smoother in both if the script switched from `setInterval` to `requestAnimationFrame`.