> As the verification process itself becomes automated, the challenge will move to correctly defining the specification: that is, how do you know that the properties that were proved are actually the properties that you cared about? Reading and writing such formal specifications still requires expertise and careful thought. But writing the spec is vastly easier and quicker than writing the proof by hand, so this is progress.
How big is the effort of writing a specification for an application versus implementing the application in the traditional way? Can someone with more knowledge chime in here please?
It depends on what you're working on. If you're doing real algorithmic work, often the algorithm is a lot more complex than its spec because it needs to be fast.
Take sorting a list for example. The spec is quite short.
- for all xs: xs is a permutation of sort(xs)
- for all xs: sorted(sort(xs))
Where we can define "xs is a permutation of ys" as "for each x in xs: occurrences(x, xs) = occurrences(x, ys)"
And "sorted(l)" as "forall xs, x, y, ys: (l = xs ++ [x, y] ++ ys) => x < y".
A straightforward bubble or insertion sort would perhaps be considered as simple or simpler than this spec. But the sorting algorithms in, say, standard libraries, tend to be significantly more complex than this spec.
> US-centric thinking about invoicing, which makes invoicing unusable (I issue invoices only after a successful payment, because I owe tax on all invoices including unpaid)
This sounds strange. I don't think there's anything US-centric about considering an invoice to be a payment request — which makes issuing them after payment nonsensical.
> invoice to be a payment request — which makes issuing them after payment nonsensical
Most EU countries use an accrual-based VAT system, where taxes are owed on any invoice issued, paid or unpaid.
This makes issuing them before payment nonsensical, because you will end up paying taxes on invoices that will never be paid, thus ruining your business.
A proforma invoice exists specifically for the purposes of quoting and requesting payment.
Long life, high activity nuclear waste represents less than 3500m3 (one Olympic swimming pool), and this, since the start of civil nuclear electrical production in the 50's. World wide.
20 swimming pools of total waste isn't that impressive. I don't want to live near that, but I'm sure I'd we can find a place to put that in that will have minimal impact on people's lives.
Exactly. The waste isn't really a problem. But it doesn't have to be waste. That's the point. All that U235 in 'spent' silos? You can get 60x - 100x its OG power feeding it to nextgen reactors. So cool
I guess you mean the "super hot for centuries" minor actinides (Np-237, Am-241/243, Cm-242/244/245 etc..)? These are less than 1% global waste, but next gen reactors can still eat them. The majority of waste (95%+) is U-235, then Pu, which nextgen also eats.
Many magnitudes of order less than any of: all the steel, glass, aluminium, wood, or plastic, ever produced, and we aren’t yet drowning in cubic miles of any of those.
> hbm chips are now emerging as another bottleneck in the development of those models. Both sk Hynix and Micron, an American chipmaker, have already pre-sold most of their hbm production for next year. Both are pouring billions of dollars into expanding capacity, but that will take time. Meanwhile Samsung, which manufactures 35% of the world’s hbm chips, has been plagued by production issues and reportedly plans to cut its output of the chips next year by a tenth.
I think it would be super interesting to see how the LLM handles extending/modifying the code it has written. Ie. adding/removing features, in order to simulate the life cycle of a normal software project. After all, LLM-produced code would only be of limited use if it’s worse at adding new features than humans are.
As I understand, this would require somehow “saving the state” of the LLM, as it exists after the last prompt — since I don’t think the LLM can arrive at the same state by just being fed the code it has written.
I described my experience using Claude Code Web to vibe-code a language interpreter here [0], with a link to the closed PRs [1].
As it turns out, you don't really need to "save the state"; with decent-enough code and documentation (both of which the LLM can write), it can figure out what needs to be done and go from there. This is obviously not perfect - and a human developer with a working memory could get to the problem faster - but its reorientation process is fast enough that you generally don't have to worry about it.
They are very good at understanding current code and its architecture so no need to save state. In any case, it is good to explicitly ask them to generate proper comments for their architectural decisions and to keep updated AGENT.md file
From my reading, GP is saying that, if one problem is the main one, it is the problem of billionaires spending money on not-consumption. There was no praise for "excessive consumption".
> Other than criminal enforcement, I'm not sure how you'd meaningfully change the incentives for someone who is willing to throw a £5 electrical device in the gutter because they can't be bothered to take it home, recharge it and refill it with £0.20 worth of liquid.
Here in Denmark we are forced to pay a small deposit when buying bottles/cans of beverages, which is returned (in cash) when you return the bottle. The consequence is that you find zero beverage bottles lying around, since they’re collected and redeemed.
If we put a, say, similar $10 deposit on these vapes, I think we’d see the same effect here. One problem is that they’re smaller, so they’re harder to find for collectors.
reply