ivanbakel

The repo is sparse on the details unless you go digging, which perhaps makes sense if this is just meant as the artifact for the mentioned paper.

Unless I’m wrong, this is mainly an API for trying to get an LLM to generate a Z3 program which “logically” represents a real query, including known facts, inference rules, and goals. The “oversight” this introduces is in the ability to literally read the logical statement being evaluated to an answer, and running the solver to see if it holds or not.

The natural source of doubt is: who’s going to read a bunch of SMT rules manually and be able to accurately double-check them against real-world understanding? Who double checks the constants? What stops the LLM from accidentally (or deliberately, for achieving the goal) adding facts or rules that are unsound (both logically and from a real-world perspective)?

The paper reports a *51%* false positive rate on a logic benchmark! That’s shockingly high, and suggests the LLM is either bad at logical models or keeps creating unsoundnesses. Sadly, the evaluation is a bit thin on the ground about how this stacks up, and what causes it to fall short.

It is likely too late for many existing contracts with packages built-in, which probably also overlap with the longest-working (and thus most expensive) engineers.

Isn't the consensus from climate scientists that emission reductions are totally necessary, and there is no solution which is solely based on capture of greenhouse gases or cooling technologies? Even if reducing emissions is not enough, I thought it was clear that it needs to be done - and the economic impact is a necessary evil, since in reality we are just seeing the reversal of economic benefits obtained at the cost of planetary temperatures.

I don’t exclusively use vertical splits - often I opt for a four-corner split if I need more than 2 panes at a time.

But your avoidance of vertical splits likely comes for the same reasons I have a rotated screen - shrinking the vertical space in a buffer by any amount on a horizontal display quickly hits some kind of ergonomic limit where you just can’t see enough of the file at a time. I find that not only splits, but also console output, search results , etc. take up too much vertical space.

> I think most people lack horizontal space more than vertical.

Is this your own experience? I’ve personally rarely suffered for horizontal space, but very often for a bit more vertical space, especially with web-browsing now being so vertically cluttered.

I think many workflows are top-to-bottom in a way that benefits from more vertical space to keep it all in view - though development is probably exceptionally well-suited. My current setup (cribbed from an ex-colleague) is two vertical screens side-by-side, and I miss it whenever I’m working with a horizontal display.

Given this is an article about Taiwan, surely the more logical conclusion is that “Chinese” refers to the PRC? Otherwise, as you say, it makes little sense. The rest of the comment is still low quality.

This alternative interpretation doesn’t seem to have much basis either, since the author is apparently native Taiwanese, but perhaps the GP is accusing her of PRC loyalties?

>How true is this really?

I’d be interested to see a more thorough analysis, but there is a simple way to gauge this - rip out all the parts of the compiler where aliasing information is propagated to LLVM, and see what happens to performance.

I found a claim that noalias contributes about 5% performance improvement in terms of runtimes[0], though the data is obviously very old.

https://github.com/rust-lang/rust/issues/54878#issuecomment-...

This looks to have been a conflation by the GP between the volume of the unit sphere itself and its ratio to the volume of its bounding cube (which is not the unit cube.) The volume of the sphere does top out at an unintuitive dimension, but indeed the ratio of the two is always decreasing - and intuitively, each additional dimension just adds more space between the corners of the cube and the face of the sphere.

> As it is, Go is massively successful and most active Go programmers don’t mind the error handling situation. The complaints are mostly from folks who didn’t choose it themselves or don’t even actually use it.

This is a case of massive selection bias. How do you know that Go’s error problem isn’t so great that it drives away all of these programmers? It certainly made me not ever want to reach for Go again after using it for one project.

I doubt that would fix the issue. The real cause is that programmers mostly deal in fixed-size integers, and that’s how they think of integer values, since those are the concepts their languages provide. If you’re going to write a JSON library for your favourite programming language, you’re going to reach for whatever ints are the default, regardless of what the specs or type hints suggest.

Haskell’s Aeson library is one of the few exceptions I’ve seen, since it only parses numbers to ‘Scientific’s (essentially a kind of bigint for rationals.) This makes the API very safe, but also incredibly annoying to use if you want to just munge some integers, since you’re forced to handle the error case of the unbounded values not fitting in your fixed-size integer values.

Most programmers likely simply either don’t consider that case, or don’t want to have to deal with it, so bad JSON libraries are the default.

Humans have been processing foods for a long time. Milling, threshing, malting, fermentation are all traditional processing techniques which often make food easier and more nutritious to consume.

And while cultivated fruits and veggies are not pap-soft, they are significantly less fibrous than seeds, stalks, husks etc that you would get from foraged, unprocessed food. Especially our farmed leaves are much softer than grass, leaves etc, that animals eat.

Point 2) feels very weak. You could easily have getR and getTheta, but critically you could also always have had them - if they make sense as APIs, and your state is encapsulated, you can expose them at any time.

The benefit of having getters is that API consumers don’t privilege public state above any other API component, because they don’t know what’s actually the real state and what’s just under contract.

Indeed, Arabic is an abjad.

>"Lamb Weston and McCain alone control 70 percent of the market" hides that McCain holds about 30% of the US market.

What exactly is objectionable about this sentence? The two companies are clearly outlined as separate in the article, and the fact that one company holds about half as much market share as both combined is... not surprising or misleading. Would you rather have the 40-30-20-7 split more explicitly outlined, and why do you think that has a big impact on the reader's takeaway from the article?

That percentage doesn’t really explain anything. What if Apple has more revenue? What if Apple users stream less, so royalty costs per subscription are lower? In both cases the AM payout could be fairer for artists and the percentage could still be lower.

The article you cite actually claims the latter is true, so it seems looking at just that statistic is misleading.

> There is a tendency in certain areas of biology to attribute extremely minor regional variation to new species.

The article describes pretty much the opposite of this, though - the species found have no regional variation, and even overlap majorly.

If the scientists involved in the paper cited by TFA have really found a large level of genetic diversity, I don’t see the point of arguing against their definition of species. It’s not a two way street, but sufficient genetic separation is enough to establish separate species, even ones indistinguishable to human eyes.

Well the article still has a point in that the insecure PRNG is neutered for seemingly no reason, contrary to developer expectations.

But I think we should, as language developers and users, be well beyond the point of pushing out and accepting insecure defaults with a little documentation disclaimer - especially if even the Dart developers themselves can't catch misuse of their own insecure APIs in widespread tools.

At the end of the day, we don't live in a computing world where true randomness is that resource-intensive anymore, and user-facing applications should basically always be relying on it. Non-randomness should really be the opt-in, when developers can actually justify that the performance penalty is a problem. Otherwise, I don't need library authors prematurely optimising my programs at the cost of security.

(There is a similar related discussion to have about the pervasiveness of floating points in programming languages when most applications would be better served by a more expensive, but more precise, numerical representation - since they rarely do that much calculation.)

Could you clarify this? What problems would you run into just from having the default RNG be secure?

The traditional Hoare logic is the "partial correctness" form - if the program state satisfies a precondition, and executing the program terminates with some other state, then the second state satisfies the postcondition. This is "correctness" in the sense it overapproximates all executions: if the postcondition says something about the state being "good", the precondition ensures you end in a "good" state, but perhaps there are more "good" states than actually reachable ones. It's partial because nothing is said about non-terminating executions.

A more recent idea was to flip this correctness logic to get an incorrectness logic, which says if you can reach a "bad" state (this is useful for bug detection.) In such a logic, you only want to know about reachable states, so the formula gets flipped: if the final program state satisfies the postcondition, then there must be a program state satisfying the precondition that can execute the program and terminate in that final state.

The difference between these two logics is one axis of this cube. There are other possible logics: you can ask if a precondition is necessary - that is, is the postcondition only reachable from states satisfying the precondition? It turns out there are two orthogonal approaches to stating such a property, and they form the other two axes of the cube.

That's a rathee obtuse response. You can typically operate under the assumption that the compiler works correctly. The question of the GP was - what prevents the compiler from (correctly) exploiting UB to change the program behaviour from the desired one? If the Linux devs want to rely on their compilers' output, they have to somehow be obeying the contract around UB.

And on the full-fledged QWERTY layout article, this claim is called "not formally substantiated". The actual citation in your link is from a collection of essays on science, paleontology, and evolutionary theory - exactly the kind of place that such an apocryphal claim could have been repeated for the sake of a pithy anecdote, rather than a reliable source on the history of typewriter layouts.

Wikipedia editors' tendency to duplicate information in sub-section summaries is a great pain, due largely to this problem - who keeps the editorial voice, references, etc. consistent across all these non-linked articles?

I think this is missing the point of the original question, which is - why would a Mauritian feel "relief" at the return of a geographical territory which is extremely far from itself? The claims of the UK or the US are irrelevant to this reasoning.

Indeed, I would like to understand the answer to the above question better, since the only reason I can see is that Mauritius as a colony used to govern the islands, and that seems to have just been a convenience of the French that doesn't strongly justify any current claims of sovereignty. And since the UK were the ones to forcibly evict the Chagossians from the islands, it seems a double-injustice to "return" their land to another sovereign power which is equally at a distance from the islands themselves. Do the Chagossians support this claim by the Mauritian government?

>In other news, as an investor, this tells me Cloudflare is technologically ahead of the other older companies who apparently were not sure they could defend against the claims.

That feels like a highly specious takeaway from this court case. Companies settle against trolls because litigation isn't free to fight. It can make very good financial sense (and even be encouraged by investors who don't want to see a company in the courts for years, as Cloudflare was.)

I would be highly interested to see the breakdown of what it cost in manhours, fees, prizes to Project Jengo, etc. versus the payout from Sable to fight this particular case for Cloudflare, and whether they even came close to breaking even just on this case alone. Likely their decision somewhat hinged on an estimate of what it might cost to settle all other patent disputes in the future, and the belief that fighting this case is actually saving them much more money down the line (but how much?).

But the UK is nowhere near full in terms of housing. The Netherlands is the densest large country in Europe, and rocks double the population density of the UK. Despite this, the two countries have a roughly equal ratio of people to homes (~2.2). It's not as if a country actually needs that much land to build homes - humans simply don't take up that much space in terms of housing.

>is since UB is not allowed, the compiler can elide checks that would protect against UB for the sake of optimization

This is incorrect. If a check prevents UB, then the compiler isn't allowed to optimise it away, because the resulting program would then contain UB when it didn't before. Part of the compiler contract is that compilers won't introduce UB - they can only rely on UB already present in the program.

Some people think that you can "catch" UB after the fact, but that's an incorrect understanding of how it works. Once UB has occurred, there is no way to go back to a coherent program state and code which would execute after some UB is therefore irrelevant.

The article says that average order price has stayed stable, including tips and fees.

>It was not very accurate with the earliest stage, called subjective cognitive decline, when patients begin to perceive their memory to be failing. Dr. Hansson said that lower accuracy probably occurred because many people with subjective cognitive decline do not turn out to have Alzheimer’s.

That's an intriguing statistical statement to make. It implies that the test simply flags lots of positives, and the accuracy gets worse in populations where the number of true positives is low. That's not such a crime (especially due to the cost of false negatives), but I don't understand why it's framed so innocuously in this way.

It's also interesting that the article doesn't mention the false-positive/false-negative rates for the blood tests, just for the physicians' diagnoses. Is there some spin on the numbers that we're not meant to see?

This is often referred to as "row typing", and the only language I've ever used that implemented it first-class with polymorphism is Purescript[0]. It's possible to model such things in other languages with sufficiently powerful type systems, though they're normally not as nice to use.

As an aside, Purescript is one of the most fun languages I've ever used for frontend work, and I lament that Elm seems to have overtaken it in the FP community.

[0]: https://hgiasac.github.io/posts/2018-11-18-Record-Row-Type-a...

The discussion in the forum points out that the Kawaii doesn't come with any wireless capabilities (they're all trimmed off the board), so unless the console is docked, you seemingly can't control it at all. Perhaps you could come up with a separate controller connector that mates with the plugs on the console without the rest of the dock.

That requires trusting that the available source is actually what's running on the machine, which is not much better than trusting that a closed-source program is correct. Open-source software is more trustworthy not only because it's inspectable, but also because you can decide to run precisely the code you see, so there's also accountability for the code that is run.