cwzwarich

If you're talking about an L1 (specifically L-1B), it's the same process for getting a green card as an H-1B. The downside with the L-1B is that you can't switch employers.

> No. "Public health authorities" are all really clear: if you're going to wear PPE you need to do it properly. DIY cloth masks are not PPE, they're theatre, so it doesn't really matter whether you wear it or not.

Even the CDC is now promoting cloth masks:

https://www.cdc.gov/coronavirus/2019-ncov/prevent-getting-si...

Sometimes an organization is complex because it has a lot of employees, rather than needing a lot of employees because it's inherently complex. You see the same thing with large software projects.

Why do you think the same thing doesn't apply to theories? Since you mention topos theory, the double-negation topology is actually a basic construction in topos theory, used to construct a dense Boolean subtopos of a given topos.

> But remember that (as far as I know) you can do intuitionist mathematics in classical mathematics, but not the other way around.

There are a number of embeddings of classical logic into intuitionistic logic. The most popular/obvious is the double-negation embedding that maps a proposition to its double negation.

> I really would have liked a discussion of why people assumed the conjecture must be true, given that the only analogy presented was obviously not true.

I'm trained in the field (on the math side, actually at the same institution as Vern Paulsen quoted in the article), and I never got the impression that the answer was universally assumed to be true. One of the major consequences of a positive answer would have been that every countable discrete group is hyperlinear, which would have violated a well-known heuristic principle of Gromov that every property of all finitely generated groups is either false or trivial.

The frustrating aspect about the refutation via quantum information theory is that there is no obvious way to transfer the insight to also refute the consequences of a positive answer to the problem.

> This is a common misconception (or poor way of phrasing it, sorry). Compiler implementers don't go looking for instances of undefined behavior in a program with the goal of optimizing it in some way. There is little value in optimizing invalid code. The opposite is the case.

Compilers do deliberately look to optimize loops with signed counters by exploiting UB to assume that they will never wrap.

Has anybody done a study of dependencies of computations in real programs and compared the efficiency of a stack representation and a register representation?

It's strange to see an article about the progress of modularity conjectures for elliptic curves that doesn't mention either Taniyama or Shimura, and instead mentions Langlands as the originator of the idea. This is bizarre historical revisionism.

Is it really formal verification if the type system is unsound? Due to undefined behavior, a "proven pointer-to-int" may not end up being a valid pointer-to-int at runtime. Even in Haskell, the type system is actually logically inconsistent (see http://okmij.org/ftp/Haskell/impredicativity-bites.html).

> C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler.

Doesn't SeL4 need -O1 codegen to make their extraction from the generated code (and the thus the rest of the formal proof) work out?

OCaml uses .() for array access.

> Bigger problem is value type generics/const generics

How does Rust solve the ambiguities with const generics?

That's why I said "plausibly". From the TypeScript spec, it looks like it takes the Boolean grammar approach (treat it like a type expression if it's a valid type expression, otherwise don't):

The grammar ambiguity is resolved as follows: In a context where one possible interpretation of a sequence of tokens is an Arguments production, if the initial sequence of tokens forms a syntactically correct TypeArguments production and is followed by a '(' token, then the sequence of tokens is processed an Arguments production, and any other possible interpretation is discarded. Otherwise, the sequence of tokens is not considered an Arguments production.

> Furthermore, I can’t think of a place in code where the generic and comparison use cases of < or > would be ambiguous or even adjacent.

Most languages that use angle brackets for generics (e.g. C++, Rust, Swift) also allow you to explicitly instantiate generics, which leads to a syntactic ambiguity, e.g. is

    a < b > (c)

a function call or two comparisons? The usual way to disambiguate in these cases is to check whether b is plausibly a type and treat it as a generic, but this is ugly on a few different levels.

> I was under the impression that covid19 was a two step process. First the virus infects and attacks the protective layer of the lungs (causing cough and fever). Then, the damage done to the protective layer of the lungs results in an infection / pneumonia, and that's where people have respiratory problems and may be in critical condition. But at this stage the viral load is low and the virus isn't the problem anymore, the pneumonia is [1].

There are apparently a large number of cases that work differently, with hypoxemia prior to any evidence of severe lung dysfunction:

https://www.atsjournals.org/doi/pdf/10.1164/rccm.202003-0817...

There are also discussions of this phenomenon on Twitter by emergency medicine professionals from NYC, e.g.

https://twitter.com/ericleemd/status/1243613497243639809

Some of them propose that early mechanical ventilation in these patients can actually cause lung damage.

[deleted, since reading it would waste your time]

Is there anything that would cause adherents to accept that it is a failed theory? All of the false predictions so far apparently haven't moved the needle much. After a while it starts to seem more like Aristotelian natural philosophy rather than modern empirical science.

It would be different if this belief was pushed by a few isolated theorists, but it's the major focus of the field and they will likely ask for billions of dollars of new public investment for accelerators to continue the goose chase, with no promising leads from any of the previous experiments.

It would also be extremely strange to publish a result like a proof of the ABC conjecture in a third-tier journal where you are an editor (actually, the editor-in-chief) rather than a top-tier journal.

Why would you think that VLIW microarchitectures would benefit from newer process nodes more than other microarchitectures?

> The processor pipeline has its out of order execution handled by the compiler, not by hardware, so there is some debate about whether this is an in order or out of order processor.

The usual problem with these sorts of CPU microarchitectures for general-purpose computing is that they can't absorb variable cache/memory load latency. How is this one any different?

There is no ordinary compilation scheme that will solve this, even with complete omniscience, since the same function with different arguments will observe different latency. Maybe some magical feedback-driven JIT could do it, but that was tried in the Itanium era and never really worked either.

Of course you need to have them, but there's no specification of their behavior, so your only hope at compatibility is reverse-engineering the existing implementation (or just reading its code).

I don't mean a formal spec. Rust is much too complicated and asymmetric to have a formal spec of the kind that exists for other languages (e.g. Standard ML), at least using current specification methodology. It doesn't even have an informal spec, which would be required to have a real attempt at multiple compatible implementations.

Would a Rust spec that actually allows multiple compatible implementations actually be simpler than the C++ spec? There has only ever been one real Rust implementation, and a lot of Rust behaviors are just arbitrary implementation decisions, especially with subtyping in the type system and the borrow checker.

No, it doesn't circumvent context switching to the kernel. With memory protection and separate address spaces, you generally need privileged execution to change page tables. However, the raw CPU cost of a syscall exception to the kernel followed by an exception return to userspace isn't actually all that high compared to all of the work that an OS usually does on top of it.

You could test data structures (which tend to be implemented using macros), but any nontrivial subsystem of a monolithic kernel lives in a web of dependencies with other subsystems. This is especially true of Linux.

To solve this, you would need to either use a hierarchical decomposition of subsystems or do some crazy mocking to run subsystems outside of the full kernel.

There is a recent project (KUnit) to add a unit testing framework to the Linux kernel, but it remains to be seen how much adoption it will get.

Does the C# parser implement incremental parsing by just using a recursive descent parser with caching, or does it do parsing with nonterminals as lookahead?

I'm curious: why can't you do tokenization in linear time? And why not use incremental tokenization for an editor?

> Self has an even bigger legacy, the JVM is basically all the technology that made Self fast ported over to Java.

Java only became fast after the HotSpot server compiler, which was written by Cliff Click (and Micahael Paleczny / Christopher Vick) and takes a different approach than Smalltalk / Self compilers.

> People who want to track users will always find a way to do so, it's a endless cat-and-mouse game. Now they will just use cookies instead...

Isn't the new policy for local storage being copied from an existing policy for cookies? How can they switch to cookies?