"Meta’s own researchers found — in an experiment they believed was better designed than any external study done thus far — that reducing time on their platforms improved mental health and well-being, specifically depression, anxiety, loneliness, and social comparison."

I am what the article calls an "industrial software engineer" and I work on "low- to medium-assurance" projects, but have used various formal methods (alloy and TLA+) in my work to prevent and discover bugs.

I've experimented with using LLMs to generate both Alloy and TLA+ a couple times over the past years, and the problems I see are:

- They have gotten better over the last few years, but still can only produce useful results in the hands of someone who is moderately competent. Becoming moderately competent requires many hours of investment in these tools, and you will lose much of this competence if you don't keep it up. For example, I can still read TLA+ and Pluscal but can't write them without lots of referring to the docs because I only write them like once or twice a year.

- They suffer even more from GIGO than other aspects of software development. If you can't really rigorously define your problem you will get a bad model/output that only gives you false confidence. A large part of the value of doing formal methods is building the muscle for thinking rigorously. Hillel Wayne says this in several places, that doing enough TLA+ (e.g.) work gives you a much better innate sense for where there will be race conditions.

- There will still be a cultural and technical problems with integrating formal methods, and their artifacts, into the rest of your codebase and team. For example, how do you prevent drift? Will you have a CI automation that uses an LLM to detect when the spec has diverged from the code?

I'm not saying it is impossible that this will happen, and I would love to be wrong, but the general tendency I see with LLM use is to make software developers less intimately familiar with their tools, and less invested in deeply understanding their code. That bodes ill for formal methods even more than regular programming.

1. The "modern American self" is best defined by (the tension between) Franklin and Rousseau. 2. Rousseau believes X and Franklin believes Y. 3. "Modern America" (society? politics? government?) flip flops between these two, though they are "almost entirely incompatible". 4. The author claims one of them scales, and says he likes it.

I engage directly with claims 2 and 3.

I think 1 is another completely absurd simplification. I do not address it, or claim 4. I don't see how that constitutes lack of engagement or quibbling. Perhaps I could have written an essay refuting OP with many citations, but I don't think that level of work is required to constitute legitimate engagement.

I guess you're probably right that my comment is more shame than content, maybe 60/40 shame to content, I should have dialed that down a bit. Fwiw I think it's fine to be simple-minded and ignorant, I am both of those things about many topics, but then your writing and argumentation should reflect your lack of knowledge and certainty. OP's article is, otoh, full of hot air.

Also the idea that these philosophies are "almost entirely incompatible" reveals the author's complete ignorance of one of the most important influences in Western philosophy, Aristotle, for whom concordance of action and "intention" (arguably not an ancient Greek concept, but close enough for an hn comment) must be united in ethically good action.

But if your goal is not actually to understand anything and merely to sound smart on a causal reading, and perhaps try to get people to "not think so damn much and just do stuff" I guess this piece achieves its goal.

Comments URL: https://news.ycombinator.com/item?id=44995385

Points: 3

# Comments: 0

Do you have a citation that supports that claim without qualifiers?

I recently reviewed a bunch of the literature on this topic and it seems like the jury is very much still out, in some cases there is a negative correlation, in others positive, in others none at all.

- say you need a messaging system to communicate between different components - that messaging system is a 3rd party library or tool, it has no knowledge of your needs or architecture - therefore it can have no knowledge of what counts as a duplicate message, it either just blasts your message off once, or blasts them off until it gets an ack, it is up to the software you build around this component to avoid duplicate processing - so yes of course you can build "exactly once processing" on top of an "at least once delivery" system - but it still makes sense to talk about the distinction between delivery and processing, and "exactly once delivery is impossible" is still (in OP's terms) a "useful" claim

I haven't personally used kafka but it and similar systems (I vaguely recall some work by Pat Helland that may fall into a similar bucket) could possibly be said to a) constitute messaging systems, b) provide exactly once delivery semantics, in that they are less of a library and more of a framework that provide a concept of "duplicate message" that you basically buy into by using those systems.

You could then argue that "if it provides exactly once delivery it is not a messaging system", maybe there's a good argument there or maybe it's just pedantry.