Even netflix suffers from this, for a while they were great, pay them watch anything. but then the traditional publishing houses started cutting their works off from netflix in favor of running their own streaming. which had two results, a balkanization of streaming video (you can't just go to one place anymore) and netflix investing into making their own content so they have something to stream.
"AMD’s AI director reports that Claude Code has become “dumber and lazier” since February, based on analysis of 6,852 sessions and 234,760 tool calls, which is the most thorough performance review any AI has received and rather more than most human employees get."
Are there any good ways to measure agent ability? Or do we just have to go by vibes?
Master/slave is almost always misused anyway. Yes one database will do all the work(we will call that one master) and the other will sit around all day waiting to take over(we call that one the slave). me nodding. yep that is about how it worked. postgres is a little closer where the master process hangs around not doing much, only really there to receive new connections which it then gives to workers to process. And don't even get me started on how IDE drives misused the term, I don't mind the master/slave terminology but if used it should at least capture some of the dynamic of that relationship.
I never did understand what they felt was wrong about git master, there was no slave or even work involved. it was more like the master print of a video. you know the thing that "remasters" are made from.
Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them?
You have a program that does something and you write another program to prove it. What assurance do you have that one program has fewer bugs then the other? Why can one program have bugs but the other can't? How do you prove that you are proving the right thing? It all sort of ties into Heisenberg's uncertainty theorem. A system cannot be fully described from within that system.
Don't get me wrong, I think these are great systems doing great work. But I always feel there is something missing in the narrative.
I think a more practical view is that a program is already a sort of proof. there is a something to be solved and the program provides a mechanism to prove it. but this proof may be and probably is incorrect, as bugs are fixed it gets more and more correct. A powerful but time consuming tool to try and force correctness is to build the machine twice using different mechanisms. Then mismatched output indicates something is wrong with one of them. and your job as an engineer is to figure out which one. This is what formal verification brings to the table. The second mechanism.
> Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them?
A bug in the formal verification tool could be potentially noticed by any user of that formal verification tool. (And indirectly by any of their users noticing a bug about which they say "huh, I thought the tool told me that was impossible.")
A bug in your program can only be potentially noticed by you and your users.
There are also entirely categories of bugs that may not be relevant. For instance, if I'm trying to prove correctness of a distributed concurrent system and I use a model+verifier that verifies things in a sequential, non-concurrent way, then I don't have to worry about the prover having all the same sort of race conditions as my actual code.
But yeah, if you try to write your own prover to prove your own software, you could screw up either. But that's not what is being discussed here.
> It all sort of ties into Heisenberg's uncertainty theorem. A system cannot be fully described from within that system.
Surely you are talking about Godel incompleteness, not Heisenberg's uncertainty principle; in which case they're actually not the same system - the verification/proof language is more like a metalanguage taking the implementation language as its object.
(Godel's observation for mathematics was just that for formal number systems of sufficient power, you can embed that metalanguage into the formal number system itself.)
I think formal verification brings a bit more to the table. The logical properties are not just a second implementation. They can be radically simpler. I think quantifiers are doing a lot of work here (forall/exists). They are not usable directly in regular code. For example, you can specify that a shortest path algorithm must satisfy:
forall paths P from A to B:
len(shortest(A,B)) <= len(P)
That's much simpler than any actual shortest path algorithm.
AWS has said that formal verification enables their engineers to implement aggressive performance optimizations on complex algorithms without the fear of introducing subtle bugs or breaking system correctness. It helped double the performance of the IAM ACL evaluation code
Formal verification is just an extra step up from the static types that you might have in a language such as Rust.
Common static types prove many of the important properties of a program. If I declare a variable of type String then the type checker ensures that it is indeed a String. That's a proof. Formal verification takes this further and proves other properties such as the string is never empty.
Common static types are very effective. Many users of Rust or Haskell will claim that if a program compiles then it usually works correctly when they go to run it.
However there is a non-linear relationship between probability of program correctness and the amount of types required to achieve it. Being almost certain requires vastly more types than just being confident.
That's the real issue with formal verification, being 75% sure and having less code is better than being 99% sure in most situations, though if I were programming a radiotherapy machine I might think differently.
The chances of significant bugs in lean which lead to false answers to real problems are extremely small (this bug still just caused a crash, but is still bad). Many, many people try very hard to break Lean, and think about how proofs work, and fail. Is it foolproof? No. It might have flaws, it might be logic itself is inconsistent.
I often think of the ‘news level’ of a bug. A bug in most code wouldn’t be news. A bug which caused lean to claim a real proof someone cared about was true, when it wasn’t, would in the proof community the biggest news in a decade.
> should not the chance of bugs be about equal in both of them?
Even if it is, the verification is still very useful. The verifier is going to run for a few minutes and probably not hit many edge cases. The chance it actually hits a bug is low, and the chance a bug makes it wrongly accept your program is a lot lower. Especially if it has to output a proof at the end. Meanwhile it's scrutinizing every single edge case your program has.
The tension between spec bugs vs. implementation bugs is real. But i will take a bug in a situation where the implementation has been verified any day.
Working over what we really want is problem solving in the problem domain.
As apposed to going into the never ending implementation not-what-we-were trying to solve weeds.
Now I am searching to see if there were models of player pianos intended to punch tape.
I have never really thought about it but a player piano sort of implies it can only play the roll. If pressed I would guess that player piano rolls were cut by hand. I mean, I am sure they had tools to help them and probably fully automatic duplication machines. but did anyone play the piano to get a piano roll? or was it more like transcribing sheet music?
here were pianos that could punch a roll, but they were rare - AFAIK there were one offs that the company who made rolls used. The better rolls labels "as played by [someone famous in 1920]" were played on such a system. Once in a while those rolls were used directly in a performance, but the most common use was an expert would use that as the master and then correct all the errors because the transcription system wasn't very accurate (I'm not sure in what way, only that the companies always had an editor make adjustments before selling those roll)
Some of them are on exhibit in a museum - but with a sign saying something like "this will never be restored because it exposes the user to poisonous mercury." If you want to know more join the Musical Box society (I'm a member), or one of the other international clubs for people who collect this type of thing (I know of several but since I'm not a member I can't remember the full name)
Yes. Wine with between 10-15% alcohol by volume[1] currently has a tax of 5,41 NOK per percent ABV per liter. So a typical 0.75 liter bottle of 12% ABV wine gets a tax of 12*0.75 = 53.19 NOK, or about $5.6 / €4.8.
For booze above 22% ABV the tax is currently 9.23 NOK. So a 0.7 liter bottle of 40% ABV Whiskey or similar would get 258 NOK or $27 / €23 in tax.
And on top of that comes the usual 25% VAT, and high wages to our bartenders etc.
Prices tend to correlate strongly with wages and wages are very high in Norway for all work, so they also have some of the highest prices on basically everything. Another lol example is a Big Mac combo meal in Oslo - you're looking at around $20.
Scandinavian countries have very specific alcohol policies, though, very restrictionist, and the tax is part of this.
This is not just question of "more expensive country, more expensive stuff". Switzerland or Luxembourg are quite expensive, but you will buy affordable and good Italian/Spanish/French wine there, because these countries don't impose anywhere near as much taxation on wine.
If you’re in Romandie in Switzerland I would recommend local wines, that’s one thing the whole French speaking region is well known for (source: I’m from there)
Is that in Oslo or elsewhere? Have prices gone down for some reason?
EDIT: Ahh! I was basing my statement on data from quite a number of years back, and just assuming prices tend to go in one direction in inflationary economies. The nuance here is that the NOK has weakened somewhat dramatically against the dollar, so relative prices aren't quite as insane now as they were in the past.
These code base cad systems are pretty great. But all of them are imperative languages and as such can only solve imperative constraints. Including declarative constraints would be very welcome. I mean, sure, Theoretically we could enter the turing tarpit and build our own constraint solver, but it would be nice to see one included as a standard library.
I am trying to think of an example, declarative constraints are usually the domain of a graphical cad system(like solvespace). but I suspect it would look like a set of relationships you can enter in any order and it solves for the missing one. so... prolog? has there ever been a cad system in prolog?
The constraints solving took a good amount of thinking while designing FluidCAD. At first I tried to make it all declarative where user just create unconstrained geometries then define constraints, something like:
const l1 = line();
const c1 = circle();
// define constraint
l1.length(100).position(x, y).tangentTo(c1)
...
Then I decided against this idea because it results in too much typing + the constraint solver implementation is not trivial and there is not much web based open source solvers. I went with a mixed approach instead between declarative and imperative. https://fluidcad.io/docs/guides/sketching/constrained-geomet...
I had a blackberry passport and it had a lot going for it(best keyboard ever on a phone) but one thing I really liked for reasons I don't understand is it had a square screen and took square photos.
Human eyes have a viewport that's like a mailslot, though. A lot of screens are a compromise between area and a movie screen like wide immersive image.
CRTs might have actually liked being nearly hemispherical because glass and deflection-from-center.
Square (or squarish) formats were pretty standard in pro photography once upon a time. Bliss, the Windows wallpaper, was shot on a camera that shoots in 6x7 natively (that's a nominal 6cm x 7cm, really it's more like 55mm x 65mm) A lot of other medium format cameras also shot in 6x7 or 6x6. And of course, 8x10 is still the standard "medium size print." I find square (or squarish) easier to compose with than wide ratios. Street photography, portraits, and sports photography don't often benefit from wider ratios, to name a few examples.
I understand what they mean, linux offers freedom, enough that it divorces your tech stack from any one company.
But isn't linux US tech? The blueprint, UNIX was a US project, torvolds works from the US. the original userland GNU was a US based project. The new userland systemd is a US based project.
reply