I've had discussions around this with theorem prover types (OPLSS, highly recommend for people who can take the two weeks off)
The sort of head canon for any of the automated proof systems is that lean saying a proof is correct is "if lean is correct then the proof is correct".
One can get the temptation to try and prove lean correctness with lean but I believe _that_ is impossible due to the incompleteness theory.
_But_ the discussions I had, everyone was kind of in agreement with the idea that you could continue to shrink down the "kernel" of lean with lean (or whatever proof system really) so that in the end the thing you have to trust is pretty small.
I think lean can verify it implements its own rules, but not that its own rules are sound (you can't prove a contradiction). If you are just prepared to trust that the rules are sound, then you would be able to trust leans implementation (if you had that Lean proof that it implements its own rules)
I don't know if we can really be clear about the order of things, but I think even without AI maths is filled with "someone provides a proof of X, and the proof itself is wrong/incomplete but X itself is true".
"Incomplete" proofs might be a way of viewing this. You have a NL argument to prove X. It turns out the NL proof has holes you can drive a truck through. So... you go around and patch the holes.
The resulting proof is different! You can start off with a bad proof and find a correct proof. Sometimes.
EDIT: for French speakers (maybe autodub gets you there) I saw a very nice simple case of this recently. A commonly stated proof for a relatively simple theory. The proof has a giant hole in it, and completing it requires some work [0])
I've always believed the opposite: get conditionals deep in your code so that the higher level control flow is regular.
But I suppose my greater philosophy for making code that avoids bugs is that you have a couple things that are done when dealing with data:
- distribution
- deciding
And you want to avoid distribution and deciding being mixed together in the same spot.
"Distribution" can be for loops but also breaking up some data based on some key into N bistinct buckets
"Deciding" is where you're looking at the data more closely to make some decision (like "is this a big customer or a small customer")
Distribution often involves decision making, but if you mix them all in one spot you can obfuscate your decision points. Splitting it up just makes things "obviously" right or "obviously" wrong. Perf stuff is another discussion of course, but in practice most things are not at a scale where it matters.
by_category = defaultdict(list)
for d in data:
by_category[category(d)].append(d)
for category, per_category_data in by_category.items():
do_thing(category, per_category_data)
I really value code patterns that make mistakes obvious, or at least makes it harder to stuff a mistake in somewhere. Some patterns are harder to describe in this model though.
(I do like the advice of having a consistent vocabulary for working on collections as a principle though, I just find that top-level conditional use tends to quickly get you into "... why is this method not called" territory, which is a more annoying problem than "why is this slow")
Your category() function contains the branch. So you pushed the condition up, and later loop through each bucket with its corresponding function. So you pushed the loops down. This is typical data oriented programming.
That's another good way to look at it - sometimes the "base" is more like a physics substrate. Physics doesn't care about semantics, it just is. Putting semantics first would be weird.
If the data don't need to be processed in batches by category, and if the category is derivable from an data item alone, I don't really see the benefit you're proposing.
Even worse, by splitting one state (and one derivable category from that state) into two separate arguments for do_thing, something can be off rather badly. I'd then feel the need to design an assertion of the relation of the arguments in order to make things bearable again:
def do_thing(category, data):
# to avoid shadowing lets rename your function `category` to `category_from_item`
assert all(category == category_from_item(item) for item in data)
...
But that would add a third loop to your two loops, and would duplicate the computation of a category.
Instead, if category would be a property of data item:
class DataItem:
@property
def category(self):
...
...and the do_thing function would work on a single data item, then it'd just become a simple matter of one for loop and one match/case:
def do_thing(item):
match item.category:
case ...:
...
For a server using a DB, all of your methods are calling out to data stores. So you're like "OK I receive a &connection" but all the mutability is hidden inside.
There's a bunch of type direction you can do to get around this (`ReadConnection` vs `ReadWriteConnection` and some other magic), far from an immediate win but it's not impossible.
People talk about mutability a lot but the vast majority of Python code I see in the wild is SSA and has _very_ little mutability to begin with.
Of course ownership still has its costs. Lots of "I guess I'm copying this dict because I don't know if the owner will modify it or not" issues.
I think people overestimate how much they'll get from `&mut` annotations on business logic, and undersestimate how much line noise they'd get from a lot of the other stuff that happens in a lot of business logic.
Granted, I'm coming from a web-dev/Django perspective, where duck typing and overriding methods in subclasses is used heavily. And a lot of that doesn't have a nice 1:1 equivalent in the Rust model.
(I enjoy Rust BTW, just don't feel particular excitement about shuffling around strings in it)
not everyone is writing simple web servers :) and if you are, then the rust is easy to read as it's simple. I also use django in some large projects, and don't see a future of my use of django really anymore. If I'm not feeling like rust is a great fit, I usually reach for Java with javalin.
I feel like everyone already knew the code was the easy part, even pre-AI.
> Coding being so easy now has just pulled back the curtain and shown the world that software developers really don't have much left to contribute. It's been done, a thousandfold.
Maybe, but I feel like there's a reason that the "useful" AI-generated work all seems to come from people who could get to the same result given "infinite" time anyways.
AI tool usage reflects and amplifies your own skill sets IMO, and I think it's pretty hard to be amazing at software architecture design but be bad at coding.
> I feel like everyone already knew the code was the easy part, even pre-AI.
I don’t agree with this at all. There still tons of buggy software around, and we ship multi-gigabyte electron installs that make fanspeeds go high and are way less efficient than software written 20 years ago.
Also the largest problem of AI written code is that is so hard to maintain, so no, coding is not the easy part.
I think it is the other way round. Building requirements from many sources of data and view points is the easy part. Implementing great, maintainable systems out of them needs specialists.
I agree there's a bunch of buggy software, my contention is that a lot of that exists is because people are bad at the hard part and the easy part!
I am also dissatisfied at the current state of software so feel your pain. I think it's just that like .... I think if you can't get the code right you're probably not getting the requirements etc right either.
The lack of polish is usually in the actual usability of the feature set (see yesterday's "polished photoshop clone" where the keyboard shortcuts just don't work)
I think you can use these tools to get something very polished. I have found that a lot of people get "tricked" into thinking that their result is good, but the people making these things and the people with expertise in the domain are often not that close to each other.
It is valuable for a thing to get used to figure out if it's actually any good.
Though the obvious glib thing is a lot of people build these tools and then don't use it.
(No not you, person who decides to reply to this saying 'but _I_ use it')
I guess it has to be said: it is not guaranteed that the water rains in the "right" spots for it to be useful freshwater again anymore. Dumb example: maybe the wind currents mean that the water simply comes back down downstream.
One shouldn't assume that evaporated water comes back into the system in the place you want it to. Water management orgs try to reduce loss from evaporation for a reason!
You're literally on a thread just a comment or two from the water cost of producing ethanol. Why are you still talking about data center water evaporation? This is morally equivalent to worrying about the water consumption of Slip-N-Slides. Everything is a rounding error compared to agricultural misuse of water.
OK sure but this is like defense in depth. It's a negligible amount of water, most of it doesn't evaporate, and most of what does rains somewhere it's useful anyway. The actual damage here is microscopic.
Median US household water usage is 130 gallons per day according to Wiki.[0]
So ~280 households worth of water? Though the US seems to be on the high end, using 3x more than Japan and 4x more than France (according to a random website)[1]
To state the obvious most people are not running big faucets all the time, and in fact are using way less.
It seems like a bit of a self-own to not just use household or per-capita usage here to prove a point though.
Framings like this are bad because people think 280 households of water is a lot.
If we instead look at almonds, something that is a bit of a luxury nut and not at all a necessity, each almond takes about 1 gallon of water to grow.
A single truck shipment of almonds contains somewhere around 40-50 million almonds all packed up ready for their delivery to Costo or wherever.
So to frame this another way, Google's DC uses approximately 1/3 of a single truck load of almonds worth of water a year. Most almonds are grown in drought stricken California as well.
I'm sure we'll be staging the protests and forgoing our emerald nuts 100 cal snack packs any day now.
No, it's just that people notice when they're being asked to concern themselves with numbers this far to the right of the decimal point. It's not just that almonds are bad. It's that they're vastly, heroically worse than data centers, so much so that optimizing water usage at data centers is like reorganizing deck chairs on the Titanic.
If you actually care about water use, you stop producing ethanol. But nobody really cares about water; that's not what this is about.
> But nobody really cares about water; that's not what this is about.
you've hit the silent nail on the head.
The complaints about data centers are really complaints against ai and its encroachment into people's lives (more specifically, they fear for their jobs due to ai).
If people truly cared so much about the environment, where were their complaints about climate change and such?
It's the same with the recent hype about how AI going rogue or is gonna kill us all if we reach AGI.
None of these are real threats, compared to the threat of climate change, where there's a real threat of crop failures enmass due to consistently extreme weather, and coastal erosion sinking cities, etc. We'll hit this before we reach AGI no doubt.
I have a sneaking suspicion that the talk about the water consumption is a red herring intentionally spread by the PR machines of these companies because it's it reframes the debate around an aspect of the issue that is ultimately irrelevant and distracts from ones that are more important like carbon emissions, pollution, electrical/gas price spikes due to induced scarcity and ultimately how these mega projects have little benefit for the people who will experience all the negative consequences of them.
Meta recently announced that they want to put a ~2.0 gigawatt DC about 70km from where I live. The provincial government played up the ~60 million that Meta would be doing int he area and the ~250 million in annual tax revenue that they would receive but none of the conversation focused on the wasted opportunity of using the heat generated from this facility to in greenhouses that could operate year round in our cold climate.
That frustrates me because the waste heat from that single facility alone could go a long way to bootstrapping a greenhouse industry here that would go a long way to ensuring food sovereignty in the region. But of course sovereignty and self-sufficiency are antithetical to the purpose of this AI infrastructure, our government lacks the foresight or will to maximize returns from these kinds of things, and people collectively lacks the ability to think and talk about these things.
So the best we can do is inconsequential conversation about water usage.
Sorry if you think 280 household of water is not a lot and if the facts don't help your cause.
For a small locality it is a real amount of water. And if there's a draining reservoir, then that's _even more_ water being pulled out of a reservoir.
The almond discussion is tiring as well. We're not growing almonds in most of the world. The water in Montana isn't the water in Cali as well.
If the facts aren't on your side on a specific issue, at least have the courage to accept it.
> I'm sure we'll be staging the protests and forgoing our emerald nuts 100 cal snack packs any day now.
People protest golf course water usage. Water usage problems in Cali are not as big of a concern to people in Montana than water usage in Montana.
And of course there are people who think that the added buildout of data centers _for AI usage_ (people acting like "oh these data centers are just from everything", let's not kid ourselves what the source of the demand is) is a net negative. People don't think that about food.
Personally I think we shouldn't be setting up massive farms in a desert (and perhaps just figure out how to make society work in a way where during winter we accept having less fresh veggies available) either.
Data center defenders need to get better talking points, cuz they sound very silly (perhaps as silly as the arguments heard on the other side!)
Should I start running through the list of industries that use more water than datacenters?
Montana exports tons of petroleum products and beef. Should I illustrate how those industries also uses orders of magnitude more water than datacenters?
In fact, I would be impressed if you could come up with a single locale where a datacenter would be the primary water consumer. Even top 3 would be kind of impressive.
I'm not sure what you are trying to say other than "datacenters use water and I don't like it, and yeah those other industires in the area use 10-100x more, but like, I don't like datascneters so we need to focus on that"
I think the real snag is that average people have absolutely -zero- concept of how much water industry uses. Your local recycling plant washes all that dirty plastic you throw in the recycling to the tune of thousands of gallons an hour. And you're learning this right now for the first time in your life. But sure, datacenters running water through metal pipes, five alarm crisis here
What the water figures show is that water usage is not the problem of these data centers. It's a drop in the bucket, literally. Yet another way to see it is that given the average weather in Lincoln, NE (29 inches of rain annually) it rains 480 million gallons annually on the 600 acres campus that Google's data center is located on. So it would be possible to collect only 3% of this rainwater, and it would be enough to cover all their water needs. Water, at the local scale of this campus or city, is an infinitely renewable resource.
Other issues than water are far worse, like pollution associated with the manufacturing and running of all the data center gear. Water is not the issue.
I don't think React pretended like they've invented FP, and I've always heard them be pretty open about FRP work existing in the past and them leaning on it.
The sort of head canon for any of the automated proof systems is that lean saying a proof is correct is "if lean is correct then the proof is correct".
One can get the temptation to try and prove lean correctness with lean but I believe _that_ is impossible due to the incompleteness theory.
_But_ the discussions I had, everyone was kind of in agreement with the idea that you could continue to shrink down the "kernel" of lean with lean (or whatever proof system really) so that in the end the thing you have to trust is pretty small.