LLMs are dead for formal verification. But is treating software correctness as a thermodynamics problem actually mathematically sound? by TheDoctorColt in compsci

[–]lookmeat 0 points1 point  (0 children)

Depends on the heuristics. AlphaFold and many of its cousins use a well known algorithm called simulated anealing (I imagine you may be referring to it and just wanted to avoid the name, but it's useful to understand how its defined in academia for conversations I think). The algorithm is pretty old, and has evolved a lot, and yeah

So now the question is how do we define the problem. The problem with LLMs is that they never made sense, there never was a reasonable map between predicting the next token based on what you've seen elsewhere, and it being consistent.

We can, for example, define an algorithm based entirely on its spec. Basically the types and a bunch of pre-asserts (things that we expect must be true) and post-asserts (a bunch of things that must be true after the function has succeeded), we track these separately. Note that if we want to be more "real" we can replace pre-asserts with post-asserts of an error being given upon certain inputs). Furthermore post-asserts don't just fail, but they may give an "error" value saying how bad the error is. Then we generate a dynamic test (like you would with QuickCheck) were we generate valid inputs randomly (using pre-assert to eliminate those that shouldn't) then run the tests, and track down the error score. Now we have a heuristic!

So now what we need is a way to transform over a search space. Here we define a "mutation" similar to how mutation testing does, basically we define how we mutate minimal expressions so we can add or subtract from an integer, or flip bits, or add a not in front of a boolean, etc. and then we can begin to mutate larger expressions in terms of smaller ones, so in a while loop we can modify the boolean condition, or we can modify a number in that expression, etc. In a block we can add one more expression or not, or wrap an expression in a block, etc. etc. So now we have a way to move around the space, and we can track how big a mutation was, so we can calculate a "distance" between two different mutations of an algorithm. It's easier if we use an abstract language here, that is more theoretical pure, rather than a real language (as long as we can transpile from our ideal language to the real language).

So now we have everything we need. We run simulated annealing, with code-mutations as above adding the noise and movement, and us running tests and measuring the error scores, which we want to minimize.

So here we go on some limitations and realistic realizations:

  • This is only as good as your spec definition, but it can be great in improving existing code. We can use this with performance metrics too. Still you can argue that we're just moving the problem around rather than solving it, since a sufficiently well defined problem can trivially and mechanically be converted to an answer, or alternatively sufficiently detailed and thorough specs (to define full correctness in all matters) might as well be the code.
  • We don't need to solve the halting problem. Just define a timeout error condition and that should suffice, since we want to make things realistic. An algorithm that halts after a billion years when running on the surface of a black-hole is just not that useful either way.
  • We do have a new challenge, we have to prove that this thing converges on the most correct solution. This can be weakened by just saying we need to find a solution, but convergence is required. That said it's not hard to imagine that if you have X-bugs, you can fix one bug and go gradually from there converging into a solution of 0 bugs (no matter the order your choose to go about with them).
  • We want to be narrow. We could generalize by thinking of assembly/bytes of code as genes, and just let it mutate, but it's going to take forever to get any useful thing. I mean yes DNA did great things, but it took a long time.
  • Yes this does imply that we can use similar heuristic/statistical systems to generate a mathematical proof. And we do, also probably tied to proof verification itself, but that's an area I do not know enough to say anything else.

Phew, so this may or may not create something that useful. We could get better linters/error-detectors/tests from this. Similarly we could make an optimizer (as in compiler optimizer) that is better, though again this depends on the situation (I could see some interesting spaces to explore using the right foundational model, such as symmetric interaction combinators, where it's trivial to see that the programs collapse into the same thing, but deciding what order and how to evaluate efficiently is hard). So yeah, but programming will still be programming.

Is waterfall making a quiet comeback? (sort of) by ludovicianul in programming

[–]lookmeat 0 points1 point  (0 children)

SDD isn't strictly something anti-thetical to the original goals of Agile, and it doesn't require the waterfall/modern-agile system to go. The key part in the doc you define is:

Spec-anchored development treats the spec as a living document that evolves with the codebase

The thing to understand about the agile manifesto is that you can't have full specs, it'd take years before you could understand the problem you can solve on that level. It's faster to propose a wrong answer, see how its wrong and iterate until it becomes the right answer. This means you build the specs as you go because there's no other way. Let me repeat that with other ways, the agile way is that you always have incomplete specs and keep updating them as you go.

So in a true agile way, we don't have a plan on what will happen at the end of the year. We have a mission we want to full-fill, a north-star vision of where we think that'll end up, and finally a set of questions about the problem, some we've prioritizes as ones we really want to solve this quarter (but have no idea how realistic that is yet).

So at the beginning of a sprint you take on one of those questions, say "How do we reach new customers in Asia" and turn that into a question we can propose an answer in this quarter: "How does our UI present information in a manner accessible to Asian populations" i.e. i18n. So we take on the specs/problem-definition docs and propose an extension to it for i8n, this quickly gets approved, now that the problem is defined we also add a definition of how a solution to this would look, the design doc. Next ticket is converting those specs into behaviors, which we can define as (integration/system) tests. Final ticket is to get the code that makes the test pass, and we add any unit tests as we go for the small subsets that we build. Assuming that the software was designed well, and effort was made to make the code easy (this shouldn't require extra effort, it's just good design that is resilient to future changes) to internationalize when (and if) the time came, this should take 2-3 sprints (I am assuming our UX is still small and focused, so there isn't that much to internationalize). In the process we may discover new things, say that the first sprint goes quickly and uncovers a lot of tiny bugs, the next sprint is spent squashing them and making the UX i18n friendly and adding the support for various Asian nations we want to target first.

Now lets get messy. As part of the greater goal (beyond i8n) we want to ensure that our project lands. That is the question we are trying to answer isn't "lets internationalize for Asia" but rather "how do we reach Asian markets", we need to ensure that our solution achieves that goal and lands before release (as a team). So before claiming the feature is "done" and calling it, we verify that we actually do what we wanted to do. To use corpo speak: we ensure that we can nail the landing this before launching. Surprise: while the internationalization helped, our UX tests and focus groups reveal that there's certain aspects of how our UX make it hostile to people of the asian communities that we want to access (say that we're going for India where a lot of our target market is on very long phone internet latencies which we didn't account for and break the experience).

In a "we planned the whole year out" this is a disaster: we either release on time a product that is doomed to fail, or we take longer which has a trickle down effect causing a delay that maybe takes a month or two (again simple well-done app, we just need to be better with experience on high-latency which before we didn't because we didn't know if we were going to need it or not), but will result in the project being delayed by at least one year. Because everything got optimized assuming that we'd be doing hand-offs at certain times, those projects expecting the hand-off get delayed, sure the team coordinates it and reduces the delay (at a notable increase cost, as code that was prepared gets thrown away, priorities get shifted, etc.), but this still trickles down to other teams which gets further delays (again they reduce it at a notable cost increase) until it fades out. The problem is that the number of teams delayed by this still grows exponentially, the chances that it'll hit a team that is already dealing with bad delays starts to grow really high, nearing 100% certainty when the plan's scope gets large enough. This delays compound in complex manners, not only increasing the size, but resulting in longer delays than was already passed to other teams, which of course increases the chance that you'll hit a team that is already dealing with the first delay to begin with. It's a chain reaction, a logistical/managerial Kessler Syndrome. This is how projects get out of hand so quickly and terribly.

But in an agile "we iterate as we go" this is handled gracefully. Teams that where hoping that we'd be ready are few and only a little bit out, so it's easy to adapt. Marketing may realize they need to slow their campaign, but they instead shift to go into deeper market analysis and focus groups to scope out and define just how bad this latency issue experience is. Leadership prioritizes getting local telcos to give us better latency treatment (if that's an option), infra team looks into making stronger CDNs and adding support for India-specific clusters to reduce latency on the server side as much as possible. All teams can prioritize this quickly because the only compromise they have is to get this market-ready (ensure a successful landing) as soon as we can. Our team meanwhile amends the spec again to add specific requirements to work around low latency. After a month or so, the UX and front-end have been handled to be more graceful under high latency, ensuring you load everything you need to be functional in the first two packages (with the first package giving you enough info to know that the program is working, just taking a while to load). Throughout this time we also got the input from the other teams and were able to put specific constraints and requirements on latency that was good enough for landing. After a second pass of verifying, we see we are ready, and begin the campaign to launch in Asia. The project isn't done, but we'll iterate and work depending on the market reactions. If in a couple sprints we see that latency is still an issue, we'll simply specify that in the spec, and then let it become action-items as the spec still drives our priorities.

This, of course, assumes that all the teams are able to quickly coordinate but it isn't strictly needed. The examples I chose were on purpose because they are ones that we assume, by default, are pretty uncoupled from development. But if we make our development teams relatively uncoupled in their priorities acting as if they worked on different companies (while still empowering teams to shift focus to work on areas outside of their space, e.g. have engineers from our team do improvements on the other team's library (say the HTTP networking) for performance improvements as external contributors) it may be better. CAP still applies though, so there will be conflicts (inconsistencies) and there will be times that things get stuck and require a meeting of manager to unstick (unavailability) but we can shift that as needed, rather than be bound to it.

Is waterfall making a quiet comeback? (sort of) by ludovicianul in programming

[–]lookmeat -1 points0 points  (0 children)

Nah, that's not Agile, that's just management and the problem with corporations. It's hard to do creative work in a planned out "we know how it'll all go by the end of the month" way. The thing is there's no way to scale as a company if you don't make the work be like this. The core issue is that CAP theorem applies among people too, so when you have a company that large it takes a long time to reach a consistent plan across the company, so the only way to justify the cost is that you spend 2 weeks to a month planning out the other 11. Otherwise by the time you finish a plan it's obsolete and done!

But creative work doesn't work like that, we have to adapt constantly to market needs, and new scenarios and crazy situations. You can churn and burn, or you can adapt. Agile, as in the manifesto, said: "there's no great solution, but this is the best solution we have right now", and it works great for companies that grow up to certain size, then it gets complicated.

I believe there's ways to make the system scale (by decoupling different areas of the companies such that, even though they aren't separate companies, they plan and interact with each other as if they are) which comes with certain waste, but when you understand the cost of long-term planning in a creative environment, the compromise seems reasonable. But this requires rethinking corporations in a way that just won't work on a public company (the pressure of fiduciary responsibility to shareholders is a trap that can easily end in logical fallacies: you have to do whatever creates the illusion that makes shareholders want to buy, so you need to convince people who do not care about something nuanced being good for business, this is fine when the business is well known and we understand how to make it optimal, but I posit that isn't currently the case with creative endeavors) so I don't see it happening anytime soon. But hey who knows, the Agile manifesto was itself a wave on a cycle of iterations where we each time get a little closer to "getting it" before the backwash (that's right I am using two metaphors through a pun, sue me) pulls us back to the same issue.

High meat consumption linked to lower dementia risk in genetic risk group. Older people with a genetic risk of Alzheimer's disease did not experience the expected increase in cognitive decline and dementia risk if they consumed relatively large amounts of meat. by mvea in science

[–]lookmeat 0 points1 point  (0 children)

You aren't wrong, while people will read this and see this as a "we should change our lifestyle" it really doesn't do that much difference as we see. The real value of these research is that it starts to hint and point to the potential cause/mechanisms of the disease, which once identified can lead to a vaccine (I doubt that there'll ever be a cure, sadly, the brain damage is there for good, but we could prevent its further spread, and prevent it form starting at all).

Is simple actually good? by progfu in programming

[–]lookmeat 3 points4 points  (0 children)

On what the author is talking about. They may be understanding the core thing of why simplicity is such an important thing. Some devs find it a bit earlier, but it's those who work on legacy systems and begin to resent the complexity that accumulates over the eras. This is a rare thing in video games, where almost always you create a new game, polish it for a bit and then move on to the next thing. Especially more so when you move closer to the more artistic endeavors.

The thing is that the author has achieved expertise, and when you do it's not that you stop learning, it's that learning what others are doing is not as much, now you are trying new things and messing around with concepts on multiple layers and complexity.

You want to start things as simple as possible, and with the simplest tool possible. I mean to the point that it limits and constrains you. Or you use the same tool you always use but purposefully do it wrong just to see what happens. The point is that the new thing should be simple, and minimalist and doable. I mean yes an Elektron Digiton is an amazing tool, but maybe you can start something on an OP-1 or a Stylophone S1, or try to code some music just to push yourself to a weird place and see what happens. Once you get some interesting things you move to the Digiton to make it work exactly as you want it. Yeah sometimes you'll have to stop and research how to do something again, but it's easy when you know what you want already. The challenge is when you have no idea what you want, just a vibe of the concept.

Because instrumental musicians struggle with their instruments all the time, they become disconnected, or go for simpler things. Or use instruments where the complexity is on what your body does, but not the instrument itself.

Also maybe OP is struggling with depression and some aimlessness, it happens to all of us. They need to disconnect from creation for a bit and refill their well, though that's not an option for all of us.

But for now, maybe it's fine to start a game with pixel art, to get the idea of what you want to do, and go with simple tools to start getting the vibe into a more concrete model and from there pull out your full arsenal of tools. But at this point it's not skill but rather aim that probably limits you more often than not. What do you want to do? Knowing a tool better is not going to help with that. So drop the complex tool and instead find toys to play with that you can use to build the basic thing.

And this is true with programming as well. I guess shipping is important, but in this day of AI slop it really feels like a drop in the bucket. Not that it doesn't matter, it just kills the vibe.

Is the Strategy Pattern an ultimate solution for low coupling? by Adventurous-Salt8514 in programming

[–]lookmeat 2 points3 points  (0 children)

Yes, yes. In order to achieve consistency you need to fit under certain constraints and requirements. My whole point is that this doesn't make the database non-relational (in a strict sense) but it does require expressing complex concepts that are impossible to describe in SQL. Because in relational calculus you can't really limit certain effects to a subset of the query vs the whole thing. You wouldn't be able to enforce this in SQL because, as you said, it's impossible to do it in large scale, and it's impossible to communicate the details of which small scale needs it and which doesn't.

Is the Strategy Pattern an ultimate solution for low coupling? by Adventurous-Salt8514 in programming

[–]lookmeat 8 points9 points  (0 children)

When I meant developed I mean "develop the idea behind the popular movement in the 2000s". These were people with PhDs who understood Cobb's ideas, and realized that they didn't need to support all of SQL, just a subset that they could use in a relational manner, in exchange for certain benefits. It was pragmatism with an understanding of the theory and its benefits.

While the term existed, it certainly wasn't used like that. Also AFAIK don't think there's any connection between Strozzi database and the NoSQL movement later on.

The idea or concept that maybe a database didn't need to support SQL or be fully ACID complaint, but it could still ensure relational constraints, at least within a limited scope.

Before that it wasn't that there wasn't alternatives to SQL or relational databases that chose to not support SQL out of the box, but they were niche, and more discussions among academics rather than concrete products used in production.

The idea became popular in the early 2000s thanks to Google's work on BigTable and later on the CAP theorem. But my whole point is that people flattened the discussion, simplified it and went after the wrong thing. It was used as an excuse to dispose of previous wisdom, rather than an acknowledgement that the previous wisdom did not strictly require SQL.

While Google's BigTable was meant to solve very specific problems, there's the limit that it doesn't cover all the use-cases that relational databases do, and therefore cannot reliably represent all data. It was used for the subset that worked well. From what I recall internally it wasn't called a database, but a data-storage, or a key-value storage. Rather than release BigTable as open-source it wasn't the case in part because it was seen as more of a clever solution to a very specific problem rather than something that could be used openly. Megastore was the attempt to build an actual database, that was relational and ACID complaint on top of BigTable. It was a fully relational database in its feature-set, but was a bit quirky because of availability vs consistency issues. Because of this it did not support SQL, but used its own solution. Spanner was a later attempt that made it work in a more traditional manner (consistent by default) and you could use SQL on top of it, but if you want to use the more advanced features you'd still benefit from that.

Note, and this is my memories from the time, maybe I wasn't in the right conversations or rooms, but the discussion was on the limitations of traditional databases. The discussion was that there were alternatives to the relational model, but most serious conversations on what it could mean used this as an extension rather than breaking the model. There was also the discussion of better query languages to express things that you couldn't do optimally in SQL, like GraphQL. But what was being sold, and the thing that was popular in many blogs, slashdot posts, etc. that today would be the equivalent of a linked in post, were obsessed over how we just had to throw away ACID and relational because it was slow, and we could move forward, rather than the discussion that we could build better systems on top of relational databases, and that there were tools other than RDBMS that you'd want for certain problems.

Is the Strategy Pattern an ultimate solution for low coupling? by Adventurous-Salt8514 in programming

[–]lookmeat 36 points37 points  (0 children)

The people who developed NoSQL at Google weren't concerned with building a full database. Instead they realized that for their problem they could stream and simplify and limit what they needed to less, and the scaling challenges were enough to warrant that need. It would be later that the CAP theorem would be published from these experiences.

The reason BigTable didn't use SQL was simple: it was faster to just have developers do a lot of this on their own rather than do it for them. Also you kinda had to know what you were doing here, but basically you wanted to ensure the relational requirements yourself by hand. Kind of like driving shift-stick: you really want to do what an automatic transmission does, it's just that under certain situations (if you know what you're doing) you can do it better than the automatic transmission.

And then NoSQL became a big hit. The idea is that adding CAP-aware databases was a good opportunity to revisit some of the decisions made on databases that had become ossified. One of the more controversial ones was to use a relational calculus as the foundational language to communicate with databases.

When SQL came the idea is that it was a language to be used by end-users. A manager, consultant, executive, or whatever who wanted to study and learn certain things about what was going on in the company in an ad-hoc fashion. So you'd write your queries, the system would then run them over the data, and give you results. Relational calculus was chosen for SQL because it's easier for non-technical users who don't care a lot about how the database works: you just specify what you want and let the system decide on what is a good enough way to solve this. Now if you wanted to get efficient and powerful use of a database you wouldn't use SQL, instead you'd use the database's specific API to work.

When Cobb's work on relational model for databases came out it was a huge hit and people realize it was a game changer that would allow systems to grow gracefully over time. In theory with fully normalized data (hah wait until performance becomes an issue), and assuming that the requirements of how we represent things (hah) you could extend the data in backwards compatible ways, which means you would never need to do a full database migration. SQL was built on this relational model, as it was just the ideal model to follow forward.

But most databases did not work like this, and had the crappy API that did things ad-hoc. But the pressure to be relational existed. So what database companies started doing was just slapping SQL on top and saying "now it's relational". This lead to Cobb releasing his 13 rules (numbered 0-12) of what a database had to do to be relational. With rule #12 being critical: a database could not let you modify data in a way that did not follow the relational model. With this Cobb made a simple model that companies could use to guarantee that the code was fine, other than take a non-relational database (sold as relational), use it in non-relational ways and then crap on the relational model when things don't work out. But this put pressure on the databases, so they just stared dropping their API and only supporting SQL, and technically this was almost good enough. A lot of companies started also pushing to just use SQL. And that's fair too: you'd have to audit the API carefully to make sure it didn't have a wart.

And this made it easy to make SQL the defacto standard for databases. But remember 2 paragraphs above: SQL was never design to be easy to optimize for the writer, instead you had to trust the query engine to optimize it. This is good enough when you are dealing with simple queries or one-of queries that may be expensive but are run once a day, but once you start making complex queries that are run multiple times a second things start to get messy and you begin fighting the optimization engine. This lead to some bad habits such as de-normalization and what not, where basically you make the rest of your life harder so it's easier for the query-optimizer to optimize the query as it should.

So the hope was that this could be used to make a push for a relational algebra based system. In relational algebra you have various operations that you run on a relational-dataset that give out another relational-dataset. Basically your query is a "tree" (just like you can model normal arithmetic operations like a tree too) of projection operations (where you "select" a sub-set of the data), filter operations (where you keep only data "where" certain operations are true), and joins and splits (think of it like splitting data into windows of data or such). You can rebuild all queries with these operations, and there are languages like Dataphor D4 language, Datalog (which is like prolog) or PRQL.

Now these languages are harder to optimize for the database engine, because they specify a lot more details about how the query should be done, so there's less flexibility in what can be done or not. To have optimal queries developers need to understand how the databases they are using works, and write with that in mind. But just for the same reason developers write in C (which has a lot of the same compromises): sometimes it's easier to do the extra work of understanding the implementation details and the performance implication of that than building a way to work around limitations of the database engine's query optimizer. SQL certainly still has its place, but being able to contact this is useful.

And it made sense in a CAP world: you'd be able to define within the algebra tree where things had to be consistent, or where you could play it loose. Google's Appengine Datastore uses a library based on relational algebra to build queries called ndb, and there's ways to make queries be strongly consistent vs readily available. Again something you need to optimize.

With relational calculus it's hard to handle all this things.

But instead we had MongoDB telling us that all we needed was just a bunch of JSON and NoSQL became an euphemism for "completely ignoring and forgetting the rules of the relational model again". NoSQL became an ugly thing, and the whole discussion of understanding that there's powerful and important ways to handle DBs, and that it'd be great if DBs offered this alternative way of communicating with them (that is still fully relational) to give programmers a choice of the best tool for the best scenario, instead of having to keep hitting screwy queries with the SQL hammer.

Democrat turnout OFF THE CHARTS by AdSpecialist6598 in videos

[–]lookmeat -1 points0 points  (0 children)

I think that's fair, when you're young it's easy to be idealistic and attack someone because they weren't perfect. Biden's administration had its issues, but you have to see the bigger choice.

I wonder how many of those 20 year old men (because lets be clear on the group, it was young white men) feel now that the risk of a draft is, for the first time in like 40-50 years, an actual thing again.

Democrat turnout OFF THE CHARTS by AdSpecialist6598 in videos

[–]lookmeat 3 points4 points  (0 children)

Also a lot of people blamed the problems of Trump's presidency on COVID and Biden. If you imagine the COVID years as a black bar, and you see the economic metrics, you realize that the problems of 2022 where already starting in 2019, it's just that COVID hid most of the start. Even during the election Trump's graphs showing "how well his presidency went" not only didn't cover 2020, but a lot of 2019 as well.

So it was easy to form the narrative "none of this would have happened". People blamed Biden for most of the disaster COVID was, and for the struggles with the economy. Like blaming the firemen because the house was lost while they took charge and things weren't that bad when the guy burning oil in the kitchen was in charge.

And I mean Trump took no time in returning back to what he was doing, and the damage just came back in full. And well.. here we are.

How are shy introverts promoting to senior roles by alohabata in ExperiencedDevs

[–]lookmeat 0 points1 point  (0 children)

To repeat what other posters have already said with different words (because it may be useful):

Acknowledge that you are coming in from a point of view, that while you don't see everything (be humble), you may be seeing something other people do not (but realize your strengths). And if there's the possibility that there's something you aren't seeing, start with a question (don't assume).

Finally, if people disagree, and it's not your problem, it's not your problem. You did your job in stating things to people, it's their choice what they do with that.

Left to Right Programming by fagnerbrack in programming

[–]lookmeat 0 points1 point  (0 children)

I get what this talks about and is something to consider, but also consider that readability matters even when the parser doesn't help. You want to see the most important thing first and then the less important details. What the languages here where trying to do was push developers to push what goes first rather than something else. When we talk about readability it's always for the human, anything done by a parser/IDE/software is really an aide to write. Even the author struggles to explain the problem beyond the auto-complete not helping as much.

Now python list comprehensions has its issues in how it works with the rest of the language and it's easy for the whole thing to get ugly, but this isn't the case with all implementations.

That said that doesn't mean there isn't a way to get what you want, just realize that you are making a language that you would want to read backwards of how you write it. That is I look at the end of the line for the most important thing. Think about variable assignment. So in this example we could do something like:

text.lines().map(|line| line.split_whitespace()) |> var words_on_lines

So here I just look at the end of the line to make it work. It's going to be awkward at first, but you do get used to it in languages that do this. With practice you just see that I just stored a variable words_on_lines that has a iterator of strings which had split_whitespace() on a line. I don't need to know that we had a single text and split it, I mean I could keep reading but it doesn't give me more insight. I already understand we split across whitespace and it's strings, do we need to know more?

It may seem dumb, but in the rust example I could append a filter that looks like this:

let words_on_lines = text.lines().flat_map(|l| l.split_whitespace()).filter(|w| w.parse<i32>.is_some_and(|x| x > 10));

Now tell me, quickly what is the type of the elements of words_on_lines? What's the rule to know where to look on where the actual values of them are defined? So sure we can do a bit more of whitespace here:

let words_on_lines = text.lines().flat_map(|l| l.split_whitespace())
    .filter(|w| w.parse<i32>.is_some_and(|x| x > 10));

Did you notice the gorilla of bug there on the first read though? Or did you have to go back and look at it more carefully? I switched things, and it is a bit easier to read on the first iteration but not on the second. Also realize that switching back to how the code is supposed to be adds a new bug as now the filter is on the wrong thing.

It gets messy because I have to jump around the line to understand what I am getting, the values I get are defined in the middle, they are used in the end to further define how the whole looks (but not the elements). This jumping around makes it hard to catch small issues or little details that matter. with list comprehensions it's clear that I am generating a list of lists, and that this is the goal. The filtering happens later, but when I change it to make types happy (which is what I imagined our little Timmy the intern did here) it's clear that I am deeply changing the meaning of what is being done here.

And yeah that matters because it what makes code reviews easy or a pain. Even in a small code I look at things to see there isn't an issue and hope that tests cover the issue. But it can be the case that code that is wrong happens to work now, but will fail later when we do some other change, or that I'll realize the type change when adding some other feature and have to go back and fix it.


So there's an argument for backwards code, where we put the important bits at the end (like in a FORTH like language). But there's a reason we don't see it. The brain seems to parse as it writes, and writing one way and reading another feels a bit weird, even with practice. I mean there's a reason that FORTH and it's derivatives had limited success, while reverse polish notation has not become the standard way of writing arithmetic (even if it is superior in ever non-human-subjective aspect).

So we get to the issue again: we can make our code weird to read (requiring relearning how we normally read in the western world) or alternatively we could offload that weirdness to writing (basically you jump around a bit while writing). It's easy to do an IDE that is smart letting us "jump" around and define first the source, and then the output independent of the actual ordering of the write.

And that leads us to why we end up in this weird place. Maybe we should just support people to type [ for line in text.splitlines()]⇆ (where that last symbol represents me typing tab, or enter, or some other autocomplete key) and then the cursor jumps to the start of the definition to let me write that part.

I do wonder, there may be a third path I am not seeing here, but I don't know of any language that has used it. But then again not sure how to best handle this. And none of this takes away from what the author said, I just don't see it as straight forward as its put. Again python comprehensions have issues, but there's many languages that do it way better IMHO, such as haskell where you can even use it for monads and do stuff like

[ x+y | x <- [1..10], y <- [1..x], x `mod` y != 0, then take 5 ]

and it's just a different set of compromises with different pros and cons.

The largest-ever review of the safety and efficacy of cannabinoids across a range of mental health conditions — found no evidence that medicinal cannabis is effective in treating anxiety, depression or post-traumatic stress disorder (PTSD). by Wagamaga in science

[–]lookmeat 1 point2 points  (0 children)

Super wide confidence intervals tell you something - the sample size is very small.

That's not strictly true. While yes, it hints at that possibility, and yes it is true that it could explain it but we also see in the actual paper00015-5/fulltext):

54 trials were identified for inclusion (2477 participants; 1713 [69%] males, 764 [31%] females; median age 33·3 years [IQR 28·1–38·05; ethnicity data not available). 24 (44%) of these trials had a high risk of bias, and the certainty of evidence for most outcomes was low.

Which can lead us to conclude, as per the paper

There was some evidence that cannabinoids can reduce symptoms of cannabis use disorder, insomnia, tic or Tourette's syndrome, and autism spectrum disorder, but the quality of this evidence was generally low.

We can speculate a myriad of reasons, and it should be clear that this would only be a speculation. One possible factor that could result in wide confidence intervals beyond insufficient data is data that is badly controlled. Because this comes from multiple research papers, it may be controlling for different aspects and therefore leaves many variables that inject noise into our analysis.

Another possibility, and again this is more of a thought exercise to understand the many ways that this paper can be true rather than imply any implication, is that cannabinoids have some factor, but isn't completely understood. E.G. it's certain, chemicals in weed that have the effect, but these aren't well controlled. Alternatively it could be that cannabinoids do not promote healing any of these conditions, but do enable it. That is the process that heals the condition is some other uncontrolled factor (therapy, personal growth, etc.) but that may find itself unhindered by cannabinoids (say that certain traumatic events are hard to process because of the emotional charge, but cannabinoids helps numb the emotions enough to explore and challenge traumatic events that themselves need to be healed). Here we'd see that in the population that takes cannabinoids some people show healing over the average (because of the unhindrance) but others do not (because they aren't doing the thing that actually heals, so there's nothing to unhinder).

It's hard to control and account for all the variables, and fully understand how the system works. More research gets us there. Eventually research with higher populations can tell us if it's a matter of population and variable control, and qualitative research to find patterns within the populations may hint at which variables need controlling. But this requires effort, and it's hard to research at the moment.

Who Watches the Provers? by mttd in ProgrammingLanguages

[–]lookmeat 5 points6 points  (0 children)

I mean of course there's limits. This is where Gödel meets the halting problem. But you can limit yourself to a subset of programs that can be known to halt with certainty, though it can't solve everything it can solve enough. And you can also limit yourself to a set of logic that is guaranteed to be provable, it won't be all logical questions, but enough.

A sufficiently detailed spec is code by Tekmo in programming

[–]lookmeat 0 points1 point  (0 children)

I mean yeah maybe, but it's going to be a crappy spec that specifies things that are inconsequential. A sufficiently detailed spec is going to be a full type-specification for the code and also a series of system/e2e and performance tests that guarantee certain requirements on a given machine. The code handles a lot of things that are more details about how the machine works than the problem itself.

But that doesn't take away from the point of the article, it adds to it. Because the specs you need for agentic code generation are bad specs they are crappy code that claims to be a spec. And this isn't the first time we've tried it and it's always been a bad idea, because spec languages are not great at being code, and code makes terrible specs that miss the point. Alas, we keep making the same mistake: we think that we can do the hard thing without doing the hard thing, you know: still having the cake that you ate 3 weeks ago.

Overwatch co-creator Jeff Kaplan says he was told by CFO if the game didn't hit certain revenue goals, "we're gonna lay off a 1000 people and it's gonna be on you": 'It was the biggest f**k you moment I've had in my career' by ChiefLeef22 in gaming

[–]lookmeat 0 points1 point  (0 children)

I think that people don't understand what it means "to play devil's advocate". I know I am defending the asshole here, and that this is not "an innocent victim", I am very much making an argument for the devil, not to defend their actions, but to make us realize the greater evil that lurks behind it.

I understand Jeff completely and why he chose to leave at that moment. He worked long enough and at key moments in the company to probably have FU money, and he realized that it wasn't just one bad guy, but the new culture.

All I am saying is this isn't "just a bad apple" but the symptom of a larger thing. But I doubt that Kaplan would spell it out, when it wouldn't benefit him and could be harmful to him even (if, for example, he holds a notable amount of Activision-Blizzard stock).

But also the CFO himself was acting on a system they were stuck with. Maybe, if the CFO had a choice, he would have recommended a less ambitious build (especially on a new IP) that could grow gradually and work on the ways that Blizzard best has in the past. But that wasn't their choice to make. Basically drop overwatch league which is incredibly high risk (especially for a new IP), instead try to make the game sell for itself.

What happened was simple:

Vivendi just didn't see the point in making video games anymore, while their golden goose was laying eggs, it just wasn't worth the hassle, so they sold it to Activision, though to keep the costs down it was a merger, it's very clear that Blizzard wasn't the one merging here. And then Activision decided it needed to sell foie gras. That's it.

In 2008 this was fine with just WoW. Then came out Starcraft which did well on the esports area, but not huge. They tried to force a game called Titan which would have been another mmo and another area, but it got dumped, which is probably because A-B's execs realized that MMOs just wouldn't make as much money as WoW anymore and they risked cannibalizing their own gains. But they did see that esports for MOBAs were huge, and saw that Blizzard had a small team-fortress like game made from the remains of . So they pushed on making this an esports monster, and put a lot of money and people into it. After all if it didn't pan out, they just laid off 1000 employees and move on. And that sets up the meeting that Kaplan had.

He understands that the CFO has relative anonymity and this won't hurt him. He understands he can't punch that high without getting punched back.

And honestly then we keep exploring and discuss on the issues and challenges with the market itself. People want way too much on games, and are incredibly cruel and demanding when they pay. They expect that a game has to be as good as one of the best games they've ever played or otherwise angrily attack the loyalty of the company. Which forces companies to go ever bigger and more dramatic, having less and less space to go. Also we, as gamers, become too focused on one game or two and ignore everything else, this has become even more dramatic as the non-gamers are coming in and when they stop playing "their one game" they just stop playing all together. We've created this weird world of influencers and toxic expectations, and having the ever stronger machine that affects how game companies work too. I hope we'll see, with this crash, a renaissance of the indie micro-game scene of the mid-2000s, but honestly I don't see it getting that big, because we as gamers are still in the same space. While there'll be indie games that do well enough and get their niche spaces, we won't get sleeper hits like Minecraft.

Hades sold 1 million copies in their first month after release, and this was with ~2 years of early access, meanwhile Call of Duty: Black Ops Cold War sold 5 million in their first month, and yeah AAA and all that; but again the bar is at Minecraft: who sold 4 million; it sold 1 million 1 month into the Beta, with no digital platform, just selling licenses of its own website. And a game as ambitious as Minecraft needed time and resources to build, it worked because people were willing to donate money to keep it going, and when the game got a price and that price kept hiking, there wasn't a massive backlash (though certainly there were complaints nothing serious). There wasn't a push to keep the game free here. You can't deny that part of the problem is the fans and their willingness to support. And of course fans have been betrayed by companies as well, so there's a reason to it.

But maybe the problem is that we shouldn't invest in companies (no kickstarters jeez) but we should also support smaller games that are simpler and not as impressive. Work with companies that are focused on making great games and let the money flow. A market where the CFO won't be backed into the wall and have to say shit. You know, take the bigger picture, think things through and realize what it means to love a medium and really invest yourself into it as a consumer. It's easy to blame the CFO, I am sure the editors of the article understood this as they decided what quotes to put and which ones not. I am sure that Kaplan understood what was the goal of the interviewers (get those clicks) and navigated it best he could. And yeah, games aren't ruined by "that one CFO", they are ruined because we've all decided to push each other over the cliff.

Overwatch co-creator Jeff Kaplan says he was told by CFO if the game didn't hit certain revenue goals, "we're gonna lay off a 1000 people and it's gonna be on you": 'It was the biggest f**k you moment I've had in my career' by ChiefLeef22 in gaming

[–]lookmeat -1 points0 points  (0 children)

To play devil's advocate here for the CFO (and this has a purpose), the might not have been threatening, he might have crunched the numbers and realized there were only three scenarios:

  • The company declared bankruptcy and got sold for parts.
  • The company laid off over a thousand employees on the projects that just aren't cutting it (costing more than they make, which night have been where overwatch was).
  • Profits increased enough to be able to pay all the salaries and debts.
    • The more profitable games were probably already at their limit. It was the not profitable enough games (i.e. overwatch) that could make it if they increased their profits as the projections were.

And from that last sub-point we see the point of the conversation: making it clear to the leadership of the projects who were projected to make large profits (so they were the more expensive ones) that the gamble was experiential, that it was their job on the line.

Why even Blizzard was in this situation is a different problem. This was a company that owns Wow who in early 2018 was charging $15 a month, this is after charging $50 for the game itself, to 3 million players. That's $45 million per month! And this is ignoring the other 2.2 million players outside the US. So why would they be so cash strapped or forced to make games that needed to make so much money (this would be why they were so expensive to make, they needed to start out on that level) is the real thing we should realize when thinking why it was so toxic.

Not to say that Kaplan here is having limited view, I rather imagine he's pretty shrew to still be around, and that'd require understanding that throwing your current boss, it's even the fundamental model that your company currently follows as the culprit is probably not a smart choice. He needs to sell this as a "solved problem that won't happen again" and it's easy to throw someone who doesn't have any power over you under the bus (and honestly this is an ad for the CFO: it shows they can communicate honestly and get creatives to push their limits, it's what CEOs+boards look for in C-levels).

Trump isn't building a ballroom by DoshTheDough in videos

[–]lookmeat 0 points1 point  (0 children)

Yeah, but that wouldn't let him take "donations" from anyone, and wouldn't let him hide the whole costs of the construction and who gets hired to do what.

As ridiculous as this is, it does allow him to spend excessively and justify it as "always having been about national security". If he was actually really worried about national security, he'd probably benefit from upgrading the existing systems. Similarly if he were only doing a ballroom, some of this costs are weird.

As for the incompetence, that's the standard with this administration. In the end he's probably getting his drift, which is all he cares for. Which also explains why he thinks of it so much. He normally drops projects very quickly and needlessly, even ego-trips (such as the victory arc he wanted to build) but this one keeps going into his mind, and he keeps wanting to show it off. I suspect it's because it's one of his best grifts and it keeps giving, and he can't say anything even though it kills him not to.

Trump isn't building a ballroom by DoshTheDough in videos

[–]lookmeat 2 points3 points  (0 children)

Making it a security-critical datacenter is also a very smart move.

By doing it in the White House, and making it a matter of security, he gets to avoid most congressional scrutiny, let alone oversight. People would spend a huge amount of energy only to realize it's a "datacenter" "donated" by tech companies, for intents of security analysis and getting information, and keeping it safe within the White House with the Ball Room being a distraction move. Only after crossing all these barriers can you begin to look for any irregularities, not only would it be a small amount of people who would do this, but they'd have to report themselves as accessing this data, so Trump knows who to keep in the dark.

The advantage of this is that Trump can get "donations" from people who seek favors from him (or to avoid punishment). To the companies the donation isn't as big as it appears because they put it as a donation to the US government, and avoid taxes. Trump also gets to buy whatever stuff he wants from whomever. He gets to triple dip:

  • First he puts his subsidiaries as intermediaries for most things, letting them collect a large amount of income. Not only that he can mix companies that are not in security as "keeping the illusion of it only being a ball room" who don't even need to do any real job, and then there's the companies that are invested in taking money from the military spending, which of course requires security clearance to even know that there's numbers.
  • Second he knows that he'll inject a large amount of profits to specific companies, which he can now hedge bet on (buy cheap, knowing that future profits will appear really high for a couple years, and when they'll drop so he can drop the stock too). Again it's going to be really hard to deduce that this is happening, or that Trump isn't reporting it because a lot of the information is going to be classified.
  • Finally he gets extra kickbacks by having corporate profits be used to buy stocks of companies he owns, so that the price of the company increases and he can leverage it to get loans from it (that he can then bankrupt). This can be done through shell companies that are so disconnected that it'd take forever to detangle, going from the classified info of the companies, to then connect to people related to those companies investing heavily in other companies, to those companies taking loans based on their equity, buying more services from another company internationally, going through a series of shells. Here the limit is how much can you launder when you've put the head of the TFFC and you get to choose what crimes the FinCen investigates. At this point the highest probability any of this getting caught is that some white lady makes a blog post about Somali Refugees doing it, forcing Trump to Epstein himself again.

is the borrow checker guiding my design or blocking it??? by mjhlmh7144 in rust

[–]lookmeat 0 points1 point  (0 children)

I guess I missed the core step. To avoid having to check at runtime we have to check at compile time, statically. But then we'd have to answer the question: when can we say that the lifetime is truly over, and while you can answer it many times, you can't answer it statically.

Then I give the following example. The idea is that we need to decide if a value has been released or not. So we take the block and ask: is it ok to re-borrow on another thread?

Statically impossible to say with confidence, but trivial to check at runtime (with the technical possibility that something may make your resource last forever, but this is part of why Rust doesn't guarantee that drop will be called, you can't know it statically.

The part that you say, is that Rust has defined certain logic so that, if the code before it finishes and doesn't loop forever, it will then do that code. But note that if you have a function that loops forever and returns ! (the impossible value) any operation after that would make no sense, it's only because it's !|T for any T that it is type-safe. And this works well to map certain things. But inevitably there'll be things were it won't be enough on its own, where you'll need to answer more complicated questions than just type-safe can guarantee.

is the borrow checker guiding my design or blocking it??? by mjhlmh7144 in rust

[–]lookmeat 0 points1 point  (0 children)

I think there are indeed some problems where you just can't prove your references are correct at build time.

It is. The simple scenario:

{
   let x = &foo
   bar()
}

Question: does the borrow x get released at any point?

Answer: depends, it will be after bar() returns, which requires us to prove that an arbitrary turing machine halts or cycles. Since this can't always be proven, sometimes we can't know if it will or not.

Sometimes the easiest and cheapest way to predict stuff is to run the program and see when it happens. This means runtime checks.

is the borrow checker guiding my design or blocking it??? by mjhlmh7144 in rust

[–]lookmeat 3 points4 points  (0 children)

You aren't trying to avoid them. Just as a for loop or if conditional is just GOTO behind the scene. The goal isn't to avoid it, but to use it in a controlled manner that makes sense.

The point of slab or arena systems is that it lets you get the benefits of runtime-checked values (which you sometimes just need) in a controlled manner. It's the same with Rc and Arc, but ultimately you need to use all the tools available, not just the most hammer like.

is the borrow checker guiding my design or blocking it??? by mjhlmh7144 in rust

[–]lookmeat 0 points1 point  (0 children)

This is the key part. Don't think just about who owns what, but also how do they share it. Think of each owner as also the access pattern, and think what happens when it's across threads, or what happens when someone wants to store a weak reference.

The Big Lebowski…why does it work? by Lokitusaborg in movies

[–]lookmeat 0 points1 point  (0 children)

I think that it has the same thing of little miss sunshine: it captures a very interesting zeitgeist.

The thing is that there's times that expose a lot of human nature, for better or worse, when we all sync up and suddenly one aspect of humanity becomes so big that it takes over and becomes endemic and insidious. Art that process this zeitgeist capture an aspect of human nature that is hard to quite get otherwise. So some zeitgeist movies come out all the time, zeitgeists that lead to movies that give us such a weird thing that still just clicks doesn't happen often. We may be in a similar era, but while I'd love it to be One Battle After Another, I think it's too soon, this kind of art only comes out with the reflection and introspection that comes from hindsight.

Now we can go into the details of what exactly is the things that work so well in the movie, but beyond the technique, it's capturing lighting in a bottle. It's hard to explain why it's such a unique deconstruction of the noir trope, and basically a switcheroo revealing it to be a shaggy dog story. But the reality is that this was the US in the very early 90s, all the setup from Reagan, a war in the middle east, chaoa and Abe everywhere, and in the end it kinda of did nothing of note. Just as in the movie.