I would give it every example TLA+ file you can find, including PlusCal stuff (as reference). Also provide an up to date language manual and/or grammar if you have one.
By definition, outsiders don't have to pay into the system since they already have a gov't somewhere else that is dedicated to them, just like the Viennese do.
>By definition, outsiders don't have to pay into the system
They absolutely do pay into the system when they move to and work in Vienna. By outsiders in this context I meant foreign workers. I assumed that was clear from the context of the discussion.
When you move to live and work in Vienna you become part of the system since you pay income + other taxes, just like the locals, except unlike the locals, you don't get social housing.
Unless of course ... your comment was just an anti immigration dogwhsitle from the start, in which case you should just said THAT instead, and not waste people's time with cumbersome allegories masquerading as arguments.
> When you move to live and work in Vienna you become part of the system
Your entire original complaint was that this doesn't happen. I agree. The difference is I don't think merely moving somewhere should give you political representation there, and the corresponding benefits you would get. You would need to gain citizenship.
"Paying taxes" has nothing to do with it. I pay taxes whenever I travel on anything I buy. I pay taxes when I export products. I don't magically get to vote or apply for social housing because of those taxes, because I'm not a citizen.
But I do have a place where I am a citizen, and if I'm upset about "my taxes" going to foreign political systems, get this, I can just choose to not pay them. No one is forcing me to travel or work in a foreign country or export products or pay taxes to people who don't represent me politically.
---
As to "anti-immigrant", my position is straightforward: citizens of Country A should not be treated as if they were citizens of Country B merely by voluntarily "paying taxes" to Country B, for goods, labor, visas, exports, or any other reason. They must actually be a citizen of a country to get the benefit of being a citizen of that country.
This is a rule that applies to every country and all people, whether an immigrant or not: you get the benefits of citizenship when you are a citizen, and not a day before.
That's pro-citizenship, not anti-immigrant. Hope that helps.
"Citizens should be free to make their own choices for themselves and their children, especially benign ones about how to socialize and who to socialize with."
It's interesting how few governments believe this. Your rulers know what's best for you, and it's not freedom.
Is it? Wow. Yeah it’s different then but still the motivation is the same. To protect vulnerable people from doing something that’s either harmful to them or others. Same with social media. If parents want to allow their kids, sure, but sad those poor neglected souls.
It might not be a perfect implementation but it will prevent a lot of the real world harm that people are seeing.
what? that's like saying "you should implement TLS instead of HTTP"!
They do entirely different things: MLS is a key agreement protocol, equivalent to the Double Ratchet that Matrix uses for E2EE today. Matrix can use both.
MLS is an IETF standard. The server is easy to write, and easy to make scalable (no complicated merge algorithm required, unlike Matrix). Finally, individual chatrooms scale to an order of magnitude larger size vs. Matrix.
MLS is superior in every way to Matrix as it exists today if you need to implement encrypted chat rooms for your app.
Source: Guy who has implemented both, including extending Matrix to scale the server to Twitter scale (by, in essence, making it working like MLS, only worse due to the merge algorithm).
What on earth are you talking about? They do entirely different things! MLS is an E2EE protocol, whereas Matrix is effectively a conversation-syncing protocol which supports multiple E2EE mechanisms, including MLS.
Source: Guy who started Matrix, was in the room at IETF 101 when MLS was proposed and ratified it for Matrix, and has been working away on the various approaches to use MLS on Matrix.
If Matrix now supports MLS, you should ask the site owner to update this: https://arewemlsyet.com/
Based on my inspection of the Rust crate [0] as of today, it does not. YMMV.
Separately, as you well know, Matrix has its own encryption (Olm, Megolm) that competes with MLS for group chat use-cases. Why you are acting like it doesn't is beyond me.
I eliminated the ability to run multiple home servers and forced clients to submit to the server so that every update was a git-style fast forward, eliminating the ability to have merges. (This means that messages could "fail", requiring a rebase + retry, just like git. Anyway, it works.)
You need a custom Matrix client to do that, which I built on top of the Rust crate.
But I didn't release any of it because MLS is exactly that + better (faster) crypto due to how key ratchets work for group members. So I added MLS' crypto to an existing chat implementation I had which already had all of the Matrix-style chat sync implemented, and dropped my Matrix client and backend. Haven't looked back.
I mostly write lean4 now and emit proof-carrying System F Omega via rfl. It's the right level of abstraction when the droids have been pinned to theory laden symbolisms. It's also just pleasant to use.
Whoops, I literally did the same thing as this guy earlier this week, but did the testing using `claude -p` so I can identify when Claude Code would (or would not) load Skills for a particular prompt, so that I could improve the skill definition.
Who knew that using Claude to introspect on itself was against the ToS?
reply