A major problem with player-coach is that it makes the manager compete with the IC. If we solve that it'd be more workable, if not it'd erode teams from the inside.
A bad guess still costs cycles, but the penalty is smaller compared to branch mispredict in the current state. But if we have some kind of pipelining, like if we have something that assumed the speculative decode is correct, then it'll be expensive again.
The two cofounders will not be able to work for Meta. Probably it will be complicated to distribute Manus in Hong Kong, possibly Singapore too.
But Manus's IP was already transferred and in any case Meta is not legally doing business in China, so Manus will still live on, possibly get rebranded.
A missing specification in the proof of lean-zip, a lean component, is a real problem to the philosophy and practice of software verification.
To illustrate, let's say you want to verify a "Hello world" program. You'd think a verification involves checking that it outputs "Hello, world!".
However, if a contractor or AI hands you a binary, what do you need to verify? You will need to verify that it does exactly print "Hello, world!", no more, no less. It should write to stdout not stderr. It shouldn't somehow hold a lock on a system resource that it can't clean up. It cannot secretly install a root-kit. It cannot try to read your credentials and send it somewhere. So you will need to specify the proof to a sufficient level of detail to capture those potential deviations.
Broadly, with both bugs, you need to ask a question: does this bug actually invalidate my belief that the program is "good"? And here you are pulling up a fact that the bug isn't found in the Lean kernel, which makes an assumption that there's no side-effect that bleeds over the abstraction boundary between the runtime and the kernel that affects the correctness of the proof; that safety guarantee is probably true 99.99% of the time - but if the bug causes a memory corruption, you'd be much less confident in that guarantee.
If you're really serious about verifying an unknown program, you will really think hard "what is missing from my spec"? And the answer will depend on things that are fuzzier than the Lean proof.
Now, pragmatically, there many ways a proof of correctness adds a lot of value. If you have the source code of a program, and you control the compiler, you can check the source code doesn't have weird imports ("why do I need kernel networking headers in this dumb calculator program?"), so the scope of the proof will be smaller, and you can write a small specification to prove it and the proof will be pretty convincing.
All in all, this is a toy problem that tells you : you can't verify what you don't know you should verify, and what you need to verify depends on the prior distribution of what the program is that you need to verify, so that conditional on the proof you have, the probability of correctness is sufficiently close to 1. There's a lesson to learn here, even if we deem Lean is still a good thing to use.
> A missing specification in the proof of lean-zip, a lean component, is a real problem to the philosophy and practice of software verification.
Every time someone makes this point, I feel obliged to point out that all alternatives to software verification have this exact same problem, AND many, many more.
I don't dispute that verification can be a good tool, but many teams exhaust their time budget at the point of figuring out what to verify, making it less necessary to verify certain things (sandboxing, airgapping, lawyering), writing simple test code, refactoring and carefully rewriting some of the prior test code, designing and realising software architecture that's more testable, etc. A certain portion of that work can use some formal verification, but it's down beneath a long list of things that not many teams manage to get through, whether or not for good reason.
This is analogous to the fundamental problem of better automation in programming - eventually, the complexity and correctness of of the spec takes over, and if we don't manage that well, creating the spec is not that much less work than the programming part. If your program was for the wrong thing, a proof of it is also wrong.
Fully agree. I started hitting this bottleneck when I combined a low-code backend I built with Claude Code to generate web applications.
I can build applications rapidly but the requirements and UX are the bottleneck. So much so that I often like to sit on a concept for multiple days to give myself the time to fully absorb the goal and refine the requirements. Then once I know what to build, it snaps together in like 4 hours.
There are a lot of ambiguities which need to be resolved ahead of time. Software engineering becomes a kind of detailed business strategy role.
I'm curious about your learning experience, but what was the nature of your bottleneck, exactly? Was the backend perfectly fine as a backend, but Claude struggled to wire it to a frontend gracefully?
Claude does a great job generating the code. The hard part was the UX like if the app gets complex, then I want a new feature which adds more complexity on top; because of the way the application/UX is designed, it's hard to integrate that feature in a way that's not confusing to the user.
Like for example, I used check boxes to mean "include the records in the result set" but in a different section later in the flow, I have a different but similar looking view/list of records but I just want to use the check boxes to do batch delete but don't want the user to think that this means "include in the result set" in this case. So maybe instead I need a different single checkbox at the top which says "Don't ask for confirmation" so the user can just click on the normal "delete icon" on each row to delete the entries quickly without being prompted... But on the other previous view/list I allow the user to use the check boxes to both include the record but also batch delete using a single small cross at the top... But in the later section I mentioned, I don't want to do this because of the way I designed the flow, it would confuse the user and make it hard for them to track what they're doing and where they made the change (I want the selection step to be in a single place, the current page serves a different purpose). So maybe I need to change the other page as well for consistency... And use the "Don't ask for delete confirmation" approach everywhere? But there's not enough space to fit that text on those other pages...
When you solve all the hard problems, this is what coding gets reduced to. Not a hard problem but it's like lots of small ones like that which keep coming up and your interface ends up with a complex URL scheme and lot of modals and nested tabs.
everybody also ignores that even hello world isn't deterministic anymore. It just doesn't matter to execution if something broke unless it kicks back an error.
although, this is the best example of how quickly a trivality can knock so called "correct" programs over.
I think it's mainly in relation to the constraints of the game engine, and also that the game engine being flexible enough to enable the gimmicks. I haven't played DDLC and probably never will, but from what I've read about it, like games with similar core themes (not dating sim) it has some gimmicks that tend to stretch the capabilities of a closed-down game engine, sometimes requiring patches to the engine itself. In this case the game engine Renpy offers an extensive DSL that makes it easy to add story scenes, media and dialogues, but allows you to fall back to python to do some tricky things.
This. First, the employer has to worry about the returns from which they draw some money to pay you. And for you to even get paid for doing a job, the company has to fear that you won't do it if you don't get paid - in most cases, it's not from the good of heart, but an implicit or explicit threat made by you or on your behalf by other people.
The current problem is automating yourself out of the job. You creating value compounds but as soon as you’re no longer needed the fruit of that compounded value is cut off from you.
Well if you want to spend your days doing something trivial enough to be automated I guess that might be a concern.
I mean I'm not sitting around doing data entry. If I'm automating something it's not my job it's someone else's. Ad a lot of the time that someone else really has other stuff they'd rather do as well.
They don't, and as a result most don't get much if any.
For them to survive, they have to have got returns from somewhere - maybe welfare, inheritance, a day job. Someone has to have worried about the returns so they can be free from thinking about it.
And if you don't worry about returns, you will let someone extract it ruthlessly from you, that you contribute millions of value to a company that gives you nothing back. This may be fine to you at some level, but many of the people who you allow to exploit you use the resources they gain as leverage to further their selfish ends, like a certain richest man in the world who helped a certain politician buy an election at the most powerful country in the world.
reply