Comment by threethirtytwo
1 month ago
> Proving programs correct end-to-end (i.e. code to high-level properties) - as this company and others purport to do - is so difficult that humans have only been able to do it for very small programs (~10KLOC) and even then, in very specialised cases, where the programs have been written in an extra-simple way (often at the cost of performance, because performance often requires more complicated algorithms).
This is not true. It has been done. I’ve seen it done for an entire OS too. Humans are very capable of doing this. The issue is this is seldom done practically speaking because the effort is not worth the benefit when the program becomes too complex.
For simple programs and small domains it’s worth it. For example type checking. Type checking proves one aspect of your program (the types) is fully correct.
> This is not true. It has been done. I’ve seen it done for an entire OS too
That might be what pron's talking about. seL4 is only 10-20K lines of code as far as I remember. Maybe you have another OS in mind, though.
If you're talking about seL4, it is tiny and intentionally simplified. I'm not aware of programs larger than ~10KLOC that have ever been verified end-to-end.
You seem to be implying that it's a toy, which it very much is not.
https://sel4.systems/use.html
I was implying nothing of the sort. It is an important and serious kernel, but a very small one and a very simple one, which it had to be so it could be verified, like the har-realtime safety critical software I worked on and formally verified. We don't yet know how to verify non-small or non-simple software with formal proofs, and unfortunately, the gap in size between the software we can prove and the average software we write has only grown significantly over the past 40 years. If AI knows how to verify "average software", then it certainly doesn't need our help with software tasks that are far simpler. My point was that some companies are imagining an AI that can write software like humans never could and then suggesting they can help it by writing simple software tools.
It isn't a toy for sure, but I doubt that it has good scalability stories when using SMP.. I'd love to be wrong given that even phones are multicores, so feel free to correct me.
1 reply →