> if shipping faster allows for faster iterations across an idea then the silly errors are worth it.
There is more to the consideration here...
Maintenance costs compound over time, as does complexity.
If you're building something that doesn't need to last long or is really simple, sure it's worth it... But a lot of stuff does need to last a long time and continuously change.
Vibe coding is a trade off that only works up to a certain distance from the existing system. If you don't need to go far, it's great. But if you need long range then it's the wrong tool for the job at the moment.
The original quote was apparently said without an understanding of the customer base as if ad blockers were not a core piece of their value proposition.
This person doesn't understand their customer if they think it's going to bring in more money to cut ad blockers... It would bring in far less money because they would lose most of their customer base. It's not off mission: it's off Target.
I would go as far to say that ad blockers are the primary value proposition of Firefox at this point. If they lose that, I have little reason to use it on my phone or my workstations.
This smells like a Principia Mathematica take to me...
Reducing the problem to "ya just create a specification to formally verify" doesn't move the needle enough to me.
When it comes to real-world, pragmatic, boots-on-the-ground engineering and design, we are so far from even knowing the right questions to ask. I just don't buy it that we'd see huge mainstream productivity changes even if we had access to a crystal ball.
Its hilarious how close we're getting to Hitch hikers guide to the galaxy though. We're almost at that phase where we ask what the question is supposed to be.
Nope; you are quite wrong here. Most people have no idea of what Formal Specification/Verification via the usage of Formal Methods really means.
It is first and foremost about learning a way of thinking. Tools only exist to augment and systematize this thinking into a methodology. There are different levels of "Formal Methods Thinking" starting with informal all the way to completely rigorous. Understanding and using these methods of thinking as the "interface" to specify a problem to an AI agent/LLM is what is important to ensure "correctness by construction to a specification".
One may ask What good is FM? Who needs it? Millions of programmers work everyday without it. Many think that FM in a CS curriculum is peddling the idea that Formal Logic (e.g.,propositional or predicate logic) is required for everyday programmers, that they need it to write programs that are more likely to be correct, and correspondingly less likely to fail the tests to which they
subsequently (of course) must still be subjected. However, this degree of formality is not necessarily needed. What is required of everyday programmers is that, as they write their programs, they think — and code — in a way that respects a correctness-oriented point of view. Assertions can be written informally, in natural language: just the “thinking of what those assertions might be” guides the program-construction process in an astonishingly effective way. What is also required are the engineering principles referred to above. Connecting programs with their specifications through assertions provides training on abstraction, which, in turn, encourages simplicity and focus, helping build more robust, flexible and usable systems.
The answer to “Who needs it?” is that everyday programmers and software developers indeed may not need to know the theory of FM. But they do need to know is how to practise it, even if with a light touch, benefiting from its precepts. FM theory, which is what explains — to the more mathematically inclined — why FM works, has become confused with the FM practice of using the
theory’s results to benefit from what it assures. Any “everyday programmer” can do that...except that most do not.
The paper posits 3 levels of "Formal Methods Thinking" viz.
a) Level 1 (“What’s True Here”). Level 1 of FM thinking is the application of FM in its most basic form. Students develop abilities to understand their programs and reason about their correctness using informal descriptions. By “What’s True Here”, we mean including natural language prose or informal diagrams to describe the properties that are true at different points of a program’s execution rather than the operations that brought them about.
b) Level 2 (Formal Assertions). Level 2 introduces greater precision to Level 1 by teaching students to write assertions that incorporate arithmetic and logical operators to capture FM thinking more rigorously. This may be accompanied by lightweight tools that can be used to test or check that their assertions hold.
c) Level 3 (Full Verification). This level enables students to prove program properties using tools such as a theorem prover, model checker or SMT solver. But in addition to tool-based checking of properties (now written using a formal language), this level can formally emphasise other aspects of system-level correctness, such as structural induction and termination.
no ! a _design_ document. how this new thing will fit together with other things that are already existing in the system. what it’s interactions are going to look like, what are the assumptions, what are the limitations etc etc.
Honestly? I usually look at the previous implementation and try to make some changes to fix an issue that I discovered during testing. Rarely an actual bug - usually we just changed our mind about what the intent should be.
Hours worked for full time employees in EU apparently has been falling year over year since at least 2013. Maybe it has increased for part timers though?
Not sure how to square that with the fact that there’s been low productivity growth since 2008.
In the higher income countries the hours worked have fallen, however it may be that in lower income countries they have increased.
That is to say, due to more work opportunities more people have gotten jobs that count towards measured work hours and GDP. Including households who used to have one person working jobs that count towards metrics now have two.
I don’t have numbers for this though, just an informed guess.
Good point. It would be sufficient for there simply to have been an increase in % of households where both parents work. That can lead to fewer hours worked per employee, low productivity growth, and increase in household income.
Household income per capita is a bit confusing, can't blame anyone for interpreting this way. But from the glossary "Household real income per capita is the adjusted gross disposable income of households, in nominal terms, divided by the total population (source: national accounts) and by the deflator (price index) of household actual final consumption. "
Many things are missing from this picture. It uses mean not median income, which would do a better job of telling how widespread the increase is. It uses a basic inflation adjustment which doesn’t differentiate between luxury goods and services vs basic necessities. In other words it’s hard to tell to what degree this rise has benefited people in general.
All Waldorf schools aren’t created equal, but things I’ve seen are anti-vax beliefs, hard belief in mystical karmic stuff, a sort of groupthink that encourages conformity and obedience and shunning of people who question authority, and (and this one is really strange IMO) a prohibition on fantasy play among the children (eg you aren’t allowed to pretend you’re running a restaurant and your friends are guests —- for reasons of crackpottery).
The problem with spaces like this is that manipulative people easily take over the rudder for the whole school combined with that it attracts a certain kind of free-thinking and liberal people who get wooed in and enable it all.
Edit: there is a Swedish documentary about one of the schools my brother went to.
Those are some big numbers. It makes me think of a crazy thought experiment:
How many MW could a container ship carry by literally shipping energy stored in batteries?
As in they fill up entirely with batteries, sail to a desert, plug into a cable to charge on cheap solar, charge up, sail to a population center, plug in to discharge. Repeat.
That's easy to work out from the parent comment. They conclude that 16,000 tons of batteries are needed for propulsion, with a total capacity of 3GWh.
For a typical 40kton cargo ship, that leaves 24,000 tons for more batteries, for a energy cargo capacity of 4.5GWh. The average US citizen uses ~770,000 BTUs of energy per day, or 0.23MWh. This "energy cargo" of this ship would provide the entire energy needs of a city of 20k people for one day. (I am being a little unfair, by assuming that everyone uses electricity for all of their energy needs in this scenario).
I think there are some startups working on cargo train "tankers" in the US too.
An idea I had after seeing the tanker concept was to have the battery carrier also serve as a generator via wind power. If its a huge ship I suppose you could just stick a turbine on it and go where the wind is blowing. I think a more fun concept is generating power off of a smaller scale cat- or trimaran generating both propulsion and power by sailing conventionally.
At 170Wh per kg (and ignoring the weight of the containers and any safety considerations), 20GWh of lithium battery would weigh 120,000 tons. This is a lot more than a typical Panamax DWT of 60,000 tons, which also needs to include the ship's fuel, provisions, crew, etc.
Momentum works well so long as you have enough alignment, clarity, and certainty.
When you don't know what you're building though, the last thing you want is a heads down project that you can't change course on or kill because it has too much momentum going in the wrong direction.
There is more to the consideration here...
Maintenance costs compound over time, as does complexity.
If you're building something that doesn't need to last long or is really simple, sure it's worth it... But a lot of stuff does need to last a long time and continuously change.
Vibe coding is a trade off that only works up to a certain distance from the existing system. If you don't need to go far, it's great. But if you need long range then it's the wrong tool for the job at the moment.
reply