ivanbakel

It's missing the point of these changes to suggest that the current version is good because the error has a just-so explanation. The same code without the MutexGuard is conceptually the same, and there a mutable reference is dereferenced twice without an error. Should the programmer need to know that they themselves need to manually write the mutable-reference coercion that the compiler would normally do to unlock the same expressivity? Is this good and intuitive language design?

>Is there an example that really benefits from these features?

That question would be easier to answer if you would spell out what you don't find compelling about the article's example, beyond the fact that you can identify a reason for the error to occur.

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?

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.