ivanbakel

They tell you how many tokens are used, however, right? Otherwise you couldn't see your own token consumption.

What's interesting about the replies to this comment how readily people provide post-hoc justifications for language features that often have no essential rhyme or reason. The same is true for the prepositions which accompany verbs, which tend to vary by language, but for which every language's speaker will gladly offer you "rules" or "explanations" for when they fit. It's great evidence that we can be very good at something with no communicable understanding of what it is we actually know.

I don't see what bearing the point you're trying to make has on the above comment. The question is not "how much it costs", the question is whether or not it's reasonable for a company to institute per-seat pricing. I think it is, if you're using that company's hosted service, since the hosting burden for them does scale per-seat.

To play devil's advocate a bit: running software isn't free. If you're paying for an online service, the hosting cost to the company does scale per-seat. It's easy to say that the company only paid the cost of development once (and even then, more users = more development demand), but you're not a user of a single unit of developed software.

For streaming services, I think the development-hosting needle swings way towards hosting. Streaming video is the vast majority of their costs and efforts, so scaling prices per-user is the only sensible option. The "software" of those services is bad and interchangeable, and not what anyone wants or is paying for in the first place.

A very valid take on spec writing. It sometimes feels like the research on formal verification is like the drunkard searching under the lamppost, in that the target is often a domain which is itself well-suited to a particular kind of computer science being done on it.

However, I think there is a middle ground between the "naturally verifiable" and the difficult cases. Certain domains, like banking apps, can want correctness guarantees about UI behaviour. A closed-off app can be very normative, so in theory specs like "the user did this action and confirmed it" can be made meaningful. But tying specs to UI is a tricky thing, and it's clearly volatile in a way function boundaries are not - apps go through redesigns, styles and elements move, etc. The abstraction of a UI as a state machine isn't hard to imagine, but actually hooking a spec into the program is a problem unto itself, and the common response is to simply ignore these problematic domains and do something easier like a backend spec that doesn't have to deal with the questions that aren't PL-shaped.

The media buzz around the ills of social media are certainly tied to moderation, as well as other problems with the governance of those sites: people are really worried about the kind of offensive content that is easily accessible to, and recommended to, children. There is some recognition that the harmful suggestion algorithms are at fault, but the fact that such content is hosted at all is also a moderation problem.

>Age verification will be a significant loss for social media companies. It's going to push plenty of people away, and it provides no information that they don't already know to a reasonably high degree of certainty.

It may push some people away (though with the centralisation of the internet, I think this is easy to overstate), but the social media companies probably aren't that worried. Their bigger threat is actual legislation and punishment. Age-gating prevents the government from coming down on them for bad moderation, since they can just block users from accessing anything that might need to be moderated otherwise.

The possibility that age verification will actually give them more data or let them track you more easily is a nice little plus, but this is more stick than carrot.

> This is the work of the UK govt, not corporate lobbyists.

This is not an exclusive or. Corporate lobbyists from social media have a real incentive for pushing age verification and attestation. They benefit from public outcry and popular movements for age restrictions online, while also presenting age verification as the only solutions to the problems causing that outcry (which is to say, largely moderation problems on their own websites).

My interpretation of the parable is really just that management consultants are paid to tell you what you already know and give you the conclusions you want to hear - hence why their "solution" is non-specific and the retrospective analysis vindicates what upper management already wanted.

It's also a criticism of management-heavy offices who have lost touch with reality, but consultants are a byword for such things, so I guess the title is succinct at the cost of accuracy.

>why would the formal verification be any more correct than the program it is verifying?

It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.

Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.

>Open source didn't stop Jia Tan

How do you think the backdoor situation would have been resolved if xz hadn't been open-source?

In some discussion about Arabic rendering on another website[0], it was pointed out that the Basmala is its own codepoint in part because it is (or was?) a legal requirement on Pakistani documents and comes from an Urdu character-set. It's possible that, as a character effectively originating from and used by Urdu speakers, Apple defaults it to Nastaliq regardless of your font settings.

0: https://lobste.rs/s/7s4sjp/u_fdfd_arabic_ligature_bismillah_...

Is this a knowing joke? Switzerland's largest (very much in both senses) coin is 5Fr, around 6 USD. Not a token amount by any means, though it wouldn't even cover most public transport journeys in cities.

Natural selection can only work at the granularity of whole organisms, since they're the things that compete and reproduce. There is no finer pressure on specific concepts like efficiency, except that they may help the organism survive - but whatever solution works for the whole organism, works.

The GP is talking about DMT, not the mushroom mentioned in the article.

> What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)

A trigger in SMT lingo is nothing of the sort. It’s simply an instruction to the solver about which instantiations of a universal quantifier should be considered, with the aim of getting a proof without too many specious steps.

The statement with the trigger on it is typically an assumption from e.g. a function specification. At some point the statement with the trigger may itself become a proof obligation elsewhere in the program, but that’s something that can be handled with SMT.

This is a point I was also wondering the whole time. The vulgarisation of literature happened all over Europe at varifying times and in different stages. We don’t see these as changes in the language itself, but instead the authors daring to write the way they actually always spoke.

There’s something in bemoaning the loss of a poetic register in written language, but that’s a different and much less significant change.

>Some programming languages (Kotlin, Swift, Rust, Typescript...) already do something similar for possible null pointer access: they require that you add a check "if s == null" before the access.

For Rust, this is not accurate (though I don't know for the other languages). The type system instead simply enforces that pointers are non-null, and no checks are necessary. Such a check appears if the programmer opts in to the nullable pointer type.

The comparison between pointers and integers is not a sensible one, since it's easy to stay in the world of non-null pointers once you start there. There's no equivalent ergonomics for the type of non-zero integers, since you have to forbid many operations that can produce 0 even on non-0 inputs (or onerously check that they never yield 0 at runtime).

>The same can be done for division (and remainder / modulo). In my own programming language, this is what I do: you can not have a division by zero at runtime, because the compiler does not allow it... In my experience, integer division by a variable is not all that common in reality

That's another option, but I hardly find it a real solution, since it involves the programmer inserting a lot of boilerplate to handle a case that might actually never come up in most code, and where a panic would often be totally fine.

Coming back to the actual article, this is where an effect system would be quite useful: programmers who actually want to have their code be panic-free, and who therefore want or need to insert these checks, can mark their code as lacking the panic effect. But I think it's fine for division to be exposed as a panicking operation by default, since it's expected and not so annoying to use.

Could you clarify what's going on in the Zig docs[0], then? My reading of them is that Zig definitely allows you to try to divide by 0 in a way the compiler doesn't catch, and this results in a panic at runtime.

I'd be interested if this weren't true, since the only feasible compiler solutions to preventing division-by-0 errors are either: defining the behaviour, which always ends up surprising people later on, or; incredibly cumbersome or underperformant type systems/analyses which ensure that denominators are never 0.

It doesn't look like Zig does either of these.

[0]: https://ziglang.org/documentation/master/#Division-by-Zero

Providing a device doesn't require picking a standard issue model of phone. IT departments often support an employee's choice of phone (or at least, choice of manufacturer) provided it's compatible with management software.

Interesting that they settled on a standard model at all. The announcement implies that the university is responsible for phone maintenance and repair, which makes sense as a motivation, but is not something I would expect in itself from a cost/expertise standpoint. I would be curious to know if a Fairphone makes servicing cheap enough to warrant doing it in-house for an IT department.

It’s also tacit, but I assume it helps them to interface with a Dutch company. Did they get any financial incentive for it?

> it is not "Safe Rust" which is competing with C it is "Rust".

It is intended that Safe Rust be the main competitor to C. You are not meant to write your whole program in unsafe Rust using raw pointers - that would indicate a significant failure of Rust’s expressive power.

Its true that many Rust programs involve some element of unsafe Rust, but that unsafety is meant to be contained and abstracted, not pervasive throughout the program. That’s a significant difference from how C’s unsafety works.

> There were certainly a lot of people running around claiming that "Rust eliminates the whole class of memory safety bugs."

Safe Rust does do this. Dropping into unsafe Rust is the prerogative of the programmer who wants to take on the burden of preventing bugs themselves. Part of the technique of Rust programming is minimising the unsafe part so memory errors are eliminated as much as possible.

If the kernel could be written in 100% safe Rust, then any memory error would be a compiler bug.

No, Exchange ActiveSync (as the other commenter correctly identified it) really allows an admin to wipe your device - ostensibly of mail, but often of all other data as well.[0]

If your Outlook server disables IMAP & POP3, then the ActiveSync protocol is AFAIK the only way to get in-app emails on your phone. Admins do this so that they can forcibly wipe the device if they "need" to.

0: https://learn.microsoft.com/en-us/exchange/clients/exchange-...

What I'm most curious about, and what the docs are light on detail about: does this mean Thunderbird complies with remote deletion requests (which IIRC, the Exchange protocol suppports)? I have the impression that Microsoft makes this a requirement for Exchange implementations, which is why third-party devices and apps like Apple's Mail cooperate with those requests.

>You don't think businesses take advantage of situations for more profit?

That's not the point. Businesses are obviously happy to raise prices under the confusion of other changes, but I find it very hard to believe "accounting fees" are a plausible way to do so. People know that the register machine can do the calculations easily - it already does so. And there is a good reason for businesses not to introduce such fees, because they are directly visible to the consumer who is going to complain and shop elsewhere.

The UPS example is apples to oranges. Tariffs are poorly understood, and consumers rarely shop around for shipping - they tend to take the service given by the merchant. The agency people will show on 2 random cents on every shop is way higher.

>It's not super relevant to the discussion of whether rounding can/will be gamed.

It's very relevant. How are consumers going to react to a price like $1.03? Especially since that's almost certainly something that would previously have been priced at $1.

> Where's the law preventing stores from imposing an accounting fee for multi-item purchases, conveniently totaling a few cents?

Where’s the law preventing someone from doing this right now? I don’t think this cynicism is justified.

Similarly, if places are willing to price stuff at $1.03 for the few extra cents they’ll collect some of the time, then they can just raise prices on 99c items right now to $1 to collect the extra cent, which they don’t do because such prices have a psychological effect on the consumer that outweighs the small gain.

> I mean, feeling sand compress in subtle ways and being able to map that mentally to an object that might be hidden in the sand seems like literally touch plus normal world modelling / reasoning

That seems like a very strong claim against the paper’s results. What makes you think that the study participants located the cube with reasoning, rather than unthinking sense?

I think we can be too quick to write things off as somehow coming from conscious thought when they bypass that part of our minds entirely. I don’t form sentences with a rational use of grammar. I don’t determine how heavy something is by reasoning about its weight before I pick it up. There is something much more interesting happening cognitively in these cases that we shouldn’t dismiss.

Probably because it’s unclear what this pedantry about synecdoche contributes to the discussion. Many people (including journalists at the state broadcaster) happily refer to the whole tower as Big Ben, so that is functionally one of its names.

Is the fact that the name originates from a bell, and that the official name for the tower is different, interesting? Maybe. Is it worth “correcting”? No, for the same reason it’s not worth policing people’s use of “Google” to mean “Alphabet”.

>Is there any reason you can't spoof literally all of that?

I think that’s what is being insinuated.

>I've been drinking raw milk probably since I was 3 year old, like most kids in my relatively underdeveloped country before I moved to the US.

Why do you think this is a strong enough reason to allow a dangerous product that used to kill people onto the market? This anecdote isn't a strong empirical justification for the safety of raw milk, just like saying that you often don't crash your car isn't a good argument for the unnecessity of seatbelts. Food poisoning incidents are not that common, even in unsanitary conditions - pasteurisation is about making it so that kids don't get unlucky.