Scale. Huawei has 1.4 billion customers just in China. They have double this around the world. The US and European markets have become small for the scale of next generations telecom.
Wrong. People that live here (in the EU) need to register. I can stay with friends abroad for some time without having to tell the government, as long as I don't take up residency.
I am talking about non-EU citizens who enter some of EU countries. No matter if they stay at the hotel or privately at relatives or friends they will be registered or must register at the police.
The answer is in the link you clicked: U-boot will be maintained as the open-source project it is, with some engineers previously working at Denx going to a specific different company with the express purpose of supporting U-boot.
Your CPU (probably) has left and right variants for shift and rotate operations, which is certainly an avenue for confusion. There's a "logical" bit order that these operations follow, which starts with the MSBit and ends with the LSBit, even when the physical connections are all parallel and don't really define a physical bit order.
The Common Lisp ASH (arithmetic shift) instruction has positive shifts for left, nefgative for right.
But even if machines were like this, it would not cause any interoperatibility issue. Because it is the data links between machines which ensure that bits are transmitted and received in the correct order, not the semantics of machine instructions.
It would be something to worry about when translating code from one language or instruction set to another.
Data link and physical protocols ensure that when you transmit byte with a certain decimal value like 65 (ASCII 'A') it is received as 65 on the other end.
The bits are "addressable" at the data link level, because the hardware has to receive a certain bit first, and the one after that next, and so on.
> There's a "logical" bit order that these operations follow, which starts with the MSBit and ends with the LSBit
Well, normally when bits are numbered, "bit 0" is the least significant bit. The MSB is usually written on the left, (such as for left and right shifts), but that doesn't necessarily make it "first" in my mind.
This exactly where the confusion came from for me. I was doing bit shifts in C to fix some DMA’d I2S output data on an ESP32, and then you have the two concepts: individual integers shifted left/right and the bytes themselves. Was very confusing back then, because I was thinking „individual bits l-r vs r-l“, which is incorrect.
This is already the case. Or rather, a corporation can not (e.g.) commit murder or theft because that usually requires some physical action. That physical action will be performed by a human, who can then be found guilty. If he was ordered to do so by (e.g.) the board, the board will be held as accessory to the crime and cam also be found guilty.
The problem is just that the board can usually claim they did not know, and that they have deep pockets to afford good attorneys. To get around the first thing, you have strict liability laws.
Strict liability laws, though, are how you end up with the situation where barkeepers are criminally liable for selling alcohol to underage people, even if they could not have known the buyer was underage (and that's about the only instance of strict liability in criminal law). I personally find this very unjust and would rather that strict liability was not part of criminal law.
> a corporation can not (e.g.) commit murder or theft because that usually requires some physical action.
Not true. Consider investor-owned utility PG&E in northern California.
"While on probation [for previous felonies], PG&E pleaded guilty to 84 felony counts of involuntary manslaughter for a 2018 wildfire that wiped out the town of Paradise, about 170 miles (275 kilometers) northeast of San Francisco."
If they know about malfeasance and don't stop it, they are complicit; if they don't know about it, they are grossly negligent. In either case, they should be held accountable for the crimes. Maybe in an ideal world it would not be that way, but since we are seeing corruption run amok in corporate board rooms, it's clear they need a greater incentive to police their organizations.
What we have is a severe lack of enforcement of the laws we do have.
We do have legal mechanisms to hold the individual people criminally liable for criminal offenses the corporation commits, the problem is we don't enforce it.
Boeing just got off scott free for killing 338 people. DOJ told the judge to dismiss the case.
We've also neglected to enforce our own anti-monopoly laws for far too long, and most recently when there could have been actual, real change, we let Google go with nothing more than a slap on the wrist.
The laws aren't the problem, the corrupt and paid for DoJ is the problem.
I mean we live in a country where 'defund the police' and 'eliminate jails' are considered somewhat mainstream legal positions (In that there are many politicians elected to office throughout the country who have held these views). All of its stems from a lack of desire to enforce standards.
Given that neither the police nor jails are relevant to corporate violations of the law, do you have a point other than that you don't understand either of those?
There is already a standard of evidence for this: "Knew or should have known". Which covers needing to exercise a certain standard of care, but without the overly rigid definition of strict liability (something that tends to result in very stupid and unfair situations).
This is why dependent types work for modelling maths: you don't actually use your proofs as programs. Sure, the formalism would allow you to, but since you don't care about lemmas like "this proof and that proof are _the same_ for certain kinds of 'inputs,'" you don't run into issues with dependent types. If you try using dependent types, lemmas like the above quickly become necessary and also quickly become unprovable.
There are some theories like HoTT where it's convenient to let the same terms act as proofs while still having computational content and sometimes a distinct identity ("proof relevance"). For example a "proof" of isomorphism that might be used to transfer results and constructions across structures, where isomorphisms can be meaningfully distinct. Of course you do retain a significant subset of purely logical arguments where no computational content is ever involved and "identity" becomes irrelevant again.
You can but that ruins the fun and also misses the point. How do you know your "trivial" theorem is actually trivial? Proofs are mechanized to increase our trust into them, and it defeats the point if you have to still manually review a myriad of helper lemmas.
Yeah I guess it's more a question of methodology for me. You have several parts of a proof, and your intuition guides you that certain parts are more likely to be risky than others. Better to get those straight first since you've a higher chance of failure (potentially rendering much of the work you have already done pointless). Then you can come back to flesh out the hopefully more straightforward parts. This is as opposed to taking a purely bottom-up approach. At least that's how I often tackle a complex coding problem - I am no mathematician!
