Rust's safety guarantees are also undecidable on an arbitrary program, but Rust still proves them for safe rust code. Why so? Because safe rust code is not an arbitrary program, it is specifically forbidden from doing some things, which becomes a pain in the ass sometimes for a coder, but the result is a subset of programs you can prove safety guarantees for.
The issue is how to design a language that restricts programmers in a way you can prove everything you care for on their programs, and still don't make life of programmers unbearably difficult, because the language allows them nothing.
Most verification is undecidable, lots of it is pspace complete. That doesn’t mean very much in practice since those are worst case bounds. People regularly solve problems that are undecidable for all practical instances that they care about.
Verifying behaviour of an arbitrary program is uncomputable. However that doesnt mean you can't have proofs of behaviour of specific programs you create.
Personally i have some doubts, a lot of research has gone into the idea without much to show for it, but its a very reasonable research area.
Part of what the research shows is that correctness-by-proof has a cost in developer effort.
If there really is a vulnerability-apocalypse due to AI, and it's not just a different flavour of AI hype, the cost of having insecure software will rise to the point that the cost of dealing with insecure or incorrect code at time of creation becomes less than the cost of ignoring it until it blows up.
I doubt it'll rise so much that we'll want to face the cost of behaviour proofs for much code at all, but it's quite possible it'll rise enough that we want to do things like prove that indices are in bounds, at compile time, so vector accesses can skip checks without compromising safety.
I fear it'll just move the problem one layer up. Sure, you've now proven that the code matches the specification - but how do you ensure the specification is watertight?
See WPA2 KRACK, you could've had a formally verified WPA2 implementation and it still would've been exploitable because the flaw was the specification itself.
Rust's safety guarantees are also undecidable on an arbitrary program, but Rust still proves them for safe rust code. Why so? Because safe rust code is not an arbitrary program, it is specifically forbidden from doing some things, which becomes a pain in the ass sometimes for a coder, but the result is a subset of programs you can prove safety guarantees for.
The issue is how to design a language that restricts programmers in a way you can prove everything you care for on their programs, and still don't make life of programmers unbearably difficult, because the language allows them nothing.
Most verification is undecidable, lots of it is pspace complete. That doesn’t mean very much in practice since those are worst case bounds. People regularly solve problems that are undecidable for all practical instances that they care about.
Verifying behaviour of an arbitrary program is uncomputable. However that doesnt mean you can't have proofs of behaviour of specific programs you create.
Personally i have some doubts, a lot of research has gone into the idea without much to show for it, but its a very reasonable research area.
There's lots of things to show for the research!
Part of what the research shows is that correctness-by-proof has a cost in developer effort.
If there really is a vulnerability-apocalypse due to AI, and it's not just a different flavour of AI hype, the cost of having insecure software will rise to the point that the cost of dealing with insecure or incorrect code at time of creation becomes less than the cost of ignoring it until it blows up.
I doubt it'll rise so much that we'll want to face the cost of behaviour proofs for much code at all, but it's quite possible it'll rise enough that we want to do things like prove that indices are in bounds, at compile time, so vector accesses can skip checks without compromising safety.
I fear it'll just move the problem one layer up. Sure, you've now proven that the code matches the specification - but how do you ensure the specification is watertight?
The specification doesn't have to be.
But yeah, writing specs is usually harder than reviewing the code 4 times :)
It kinda does.
See WPA2 KRACK, you could've had a formally verified WPA2 implementation and it still would've been exploitable because the flaw was the specification itself.
Moving the problem one layer up is the desired outcome because it makes exploitation much more difficult. Your attack surface becomes much smaller.