alt Hacker NewsYou speak as if that is a software or tech problem. People cannot even stop producing direct-to-garbage fast fashion. Who can make them completely rewrite all software, so it is tractable to prove? Please consider that there has been almost no hardware nor llm architecture progress in last few years. Apparent progress is people literally burning money to buy and power the gpus.
You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
Replies
Claiming the models are not good at math at this point, especially for things like formalization where w you aren't even breaking new ground, is a very very bold claim to make. So ignoring that point for obvious reasons, why would people rewrite all software?
1. Because everything everywhere is getting hacked
2. For the same reasons people are already decomping games and rebuilding Photoshop and stuff - because they can and don't want to pay for proprietary options.
3. Because of the exact same dynamics of fast fashion? I'm not sure how fast fashion supports your point. Fast fashion is specifically not maintaining old clothes and treating all clothes as disposable slop and rotating through them. That dynamic in software is all software becomes single use throwaway and formalization as a part of the agent loop based on some set of standards is a pretty good way to make that tractable
The people don't produce fast fashion. The forces of capitalism encourage it.
> You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?
No plans on that front. Instead, I write my software from the start using a methodology of formal specification and proof. And at some point (1 year from now?) that software will include something much better and cooler than Powerpoint.
Maybe they don't need to write new software. Qubes-OS didn't need to write all linux software from the start. It just secured the infrastructure.
What if we could do that to popular web frameworks?
And than, what if we had tools that could easily define, specific security properties of web sites built on these platforms? For example, "no data ever flows between different users, unless it's via specific API call by the user's code?"
And if we can define a security property, in a specific application, for ex. slack that says "data in a chat between two group members can only go to the group manager, if the setting "manager as god" is set by both users", and the AI can formally verify that? And than have a short file defining all the security properties we want for out specific application ?
And than have AI formally verify all of that?