I'm not giving you a hard time. I'm saying that I made my choice. I'm going to stay in my home.
I don't really think those are the only three choices, though. The government can fail and be replaced with a new one that will shape things up. Then it'll be replaced by another that thinks it's too big and well off to fail, squander it, and fail. That's the typical cycle.
The problem is that you're camouflaging the implicit position of "I'm going to stay in my home, even if I have to see the world burn." as the seemingly reasonable position "I'm going to stay in my home", while being utterly ignorant to the consequences based on absurd levels of wishful thinking.
You're saying the government is going to fail, but actually it's not really going to fail. Someone is going to bail you out every single time. If the government failed, but I'm still in the house, it didn't fail hard enough. They should get better and more competent at failing. The failure needs to be more absolute and its consequences should be unavoidable. The bare minimum required is that they thoroughly crush my spirit and desire to keep living in this place.
People with a semblance of sanity left in their brain understand that getting the things they want, also means dealing with the associated costs and that if they insist on those things, they also implicitly insist on the costs associated with those things. When people refuse this cost benefit trade off, they will end up losing the things they want.
I'm trying to follow this but unclear of the root of the problem. Is it beacause building roads in L.A. is inherantly more expensive than elsewhere? I thought one of the selling points of cities was scale: costs are spread over more people. But, it sounds like road building is cheaper per resident in my small city. Sounds more like a corruption problem.
I'm suggesting that this isn't the actual answer. The thread started with the premise that the city doesn't have enough revenue, and that the way to increase that revenue is to bring in more people who pay more tax. Next, bringing in more people requires more housing, so that requires incentives for developers to displace people residing in SFH so that the can replace those with high density housing. There's a big problem: more people require more services beyond fancy curb cuts, like police, fire, water, electricity, schools, hospitals, etc. That cost that is spread also grows proportionally with the number of people, and you can't ignore that.
On the cost of building roads: there are cement and asphalt plants right in LA city proper, and also in weho and inglewood, among others in the county. LA has a price problem, not a cost problem.
There are more specters, too, which are bound to be political fights. For one, when you dig up a road, there are numerous places that will require displacing very large homeless camps. Now, credit where it's due, LA has shown that it is able to do that sometimes, like around Echo Park, which is the junction of several major thoroughfares like glendale blvd and the 101. Still, these are non-trivial projects that take years.
I find it hard to look at the actions of the Japanese and the Americans in the late 1930s and come away with any other impression than that the Americans were the good guys.
I'm not saying Japan was good, and this isn't a callout to you. I'm arguing that the erasure of US brutality in China and the Philippines, as well as Gunboat Diplomacy on Japan itself, is why we can see ourselves as the Good Guys. This erasure is part of Manufacturing Consent. Its better to abandon the temptation to moralize the sides in war and see it as Great Power competition.
First we have US [Commodore Perry] who, in 1854, used gunboat diplomacy in Nagasaki harbor to end Japan's isolation and open it up for trade. This would snowball into the Meiji restoration, which ended the Shogunate, and an Emperor that rapidly modernized Japan's economy and military to prevent foreign domination that China was experiencing at that time.
Three decades prior to Japan's invasion of China, and a decade before Japan seized Korea, the United States and other Great Powers were suppressing the Boxer Rebellion as part of China's [Century of Humiliation] to exploit China for themselves. In addition the US, after it seized the Philippines from Spain, spent several years brutally putting down the native independence movent [p-h war]. Americans aren't taught this history, and fear of that brutality of American reprisals influenced the Japanese against surrendering during WW2.
Speaking of the Philippines, its seizure by the US and other Spanish territories after the Spanish-American war as well as the annexation of Hawaii alarmed Japan. They saw US and other imperial powers as rapidly encroaching on Japanese sphere of influence, in particular the decades of 1890s-1900s. Japan saw all of this and didn't want to be the next China. Japan also saw all of East Asia was it's sphere of influence as a Japanese mirror of the Monroe Doctrine and the western imperial powers as both a tacit threat and competition.
The US wasn't interested in helping China against Japan out of a moral duty, but protecting US interests against a rising Japanese Empire, in addition to British, French, and Dutch colonies in the Far East. The tipping point for Japan was when the US embargoed Oil and ship-grade Steel (as well as other strategic commodities and economic sanctions) from Japan throughout 1941, which led to Japan planning to seize more territory in SE Asia. To support these annexations, Japan had to push the US out of the Philippines, and to do that they attacked Pearl Harbor as a way to buy Japan time to take and hold territory before Americans could respond.
I mention all of this because Americans aren't taught this yet so much of our history hinges on these events.
For comparison, in Rust they track down the differences in which flags are ignored in a certain kind of `fcntl` syscall across all the architectures that have this C function, which includes Solaris, Mac OS, the BSDs, Linux, ...
This is so that this is correctly handled in Miri, which can then be used to run the test-suite of the OS-specific parts of the standard library, and observe if this uses unsupported features in some way. This ensures that the standard library relies on documented features and not on whatever happens to work right now.
Referenced at the very end; I came here to mention the sheer size of this effort. 60,000 lines is incredible. I can barely review 1,000 lines of Python without wanting to become a manual laborer instead.
> Ten years later their approach was fully machine-checked by the French computer scientist Georges Gonthier who verified 60,000 lines of formal language proof before declaring that their proof was indeed correct
Both type and set theory are formal logic, I don't see how that's what being argued. Rather that there are some things that are formal-logicy (e.g. set theory) and many other things that are not (like e.g. biology, you'll always find some weird organism breaking your assumptions).
Depends on if the Chinese can get over foreigners messing up the tones all the time.
English has the advantage that it already had a lot of different ways of pronouncing it before becoming the world language, so the expectations for how perfect people's pronunciation should be was lower.
That’s just not true though. Sure English doesn’t have tones, but there are other tricky parts of the language. Additionally, Russian is another “difficult” language, but all the satellite nations had no problem picking it up.
The real reason people learn English isn’t because it’s easy. It’s because they need to. As someone who is married to an immigrant, it’s not easy for them. They’ve just worked really hard over decades.
Americans will do fine learning Chinese if it ever becomes an economic necessity.
It's not easy to become highly proficient in english but it's quite easy to speak just barely well enough to communicate effectively in a professional context. Importantly, the written form follows naturally from the spoken. You won't get all the edge cases right (that's incredibly difficult even for native speakers) but getting in the ballpark can be done purely phonetically with a fairly small set of rules. Combine with modern spellcheck and I expect it's pretty difficult to beat for ease of practical use.
I think at least a few of the latin based languages are in the same ballpark but for inane historical reasons it's english that won out.
Compare with chinese where even if you sweep tones under the rug you've got a bunch of idioms (difficult) followed by one of the most difficult writing systems in existence. Don't get me wrong, I think the writing system is quite elegant and has a truly impressive history, but neither of those things has anything to do with ease of mastery.
A tangential thought is that if you intentionally set out to come up with a rule following yet maximally difficult language I think a reasonable approach would be to fuse the equivalent of latin grammar with chinese tones and then fuse a chinese style writing system with arabic style contextually sensitive ligatures.
> Russian is another “difficult” language, but all the satellite nations had no problem picking it up.
Russian is not more difficult than English and a lot of the satellite states were speaking other Slavic languages.
If you already speak Spanish, it's less difficult to pick up Italian too.
There’s also the fact that a huge portion of foreign immigrants to the US don’t and won’t learn English, but can still operate just fine (or even have the system cater to them - press 1 for Spanish).
Look at the uproar over requiring commercial drivers to be able to read road signs in English.
The US also did annex large parts of what used to be Mexico in the 19th century, so you don't even technically have so be an immigrant to speak Spanish
Unless you're 126 years old, that excuse doesn't really hold up. Plenty of immigrants came from Italy, Poland, and Russia more recently than your mentioned time, but you don't hear Press 3 for Italian too often.
They didn't have to. But they also shouldn't expect the annexing government or populace to accommodate them.
Their country lost the war, lost the territory, and those that stayed and chose to take American citizenship should've learned English, the (de facto) language of the country they chose to join.
While I don't know the specifics of Lean, I know Rocq and will attempt to answer some of the remaining questions. I look forward to someone else telling me that my intuition from Rocq is completely wrong, so take this all with a grain of salt and read the comments replying to this one.
1) rfl vs doing a proof:
It depends on how your things are defined. For example, consider the function that appends two lists, a classic in functional programming (Here's a refresher: https://stackoverflow.com/a/35442915/2694054 )This is usually defined by recursion. But the details matter: The example in the link is defined by recursion on the first argument. That is, for a concrete first argument, it can evaluate. So it can e.g. evaluate `append [] ys` to `ys` just by unfolding the definition and resolving matches. But for `append xs []` you can not evaluate the `xs` any further because the remaining behavior depends on its concrete shape. So to prove that `append xs [] = xs` you need a proof (by induction).
2) Prop vs Decidable
Prop is a mathematical proposition. For example, the Riemann Hypothesis is a Prop. But a decidable Proposition is one for which you can write a program that knows if it is true or false. And you need to actually write this program, and prove it correct. So currently the Riemann Hypothesis is not decidable, because no one figured out how to write that program yet. (It will be a simple `return true` or `return false`, but which??) This mostly shows up for something like `forall x y, decidable (x = y)` which allows you to say that for any two numbers you can decide if they are equal or not. You can then use this when you actually do functional programming in Lean and actually want to run the program on concrete inputs.
The remaining two questions are more specific to Lean's engineering so I won't even attempt to answer that.
The gendarme might actually arrest the attacker. The security camera will do nothing (but record). And having the policeman standing there is about as much a deterrent as a "Smile--You're Being Recorded" sign.
It also involves being able to look the person doing the sentencing in the eye and them telling you their reasons for the ruling to the face; being able to argue and present evidence in front of a neutral arbiter.
Facebook's moderation might well be just but it lacks the accountability and openness and humanity to appear just. (It also isn't just but I'm saying that even if it was, it would not appear so.)
You might think there is option 4--municipal bankruptcy--but that is just option 2 and 3 combined.
Building buildings somewhere else will not fix your neighborhood.
reply