Earlier quoted context omitted.
This is the smoking gun for me: procedure Overflow_This_Buffer with SPARK_Mode => On is type Integer_Array is array (Positive range ) of Integer; Int_Array : Integer_Array (1 .. 10) := [others => 1]; Index_To_Clear : Integer; begin Ada.Text_IO.Put ("What array index should be cleared? "); -- Read the new array size from stdin. Ada.Integer_Text_IO.Get (Index_To_Clear); Int_Array (Index_To_Clear) := 0; end Overflow_Thi…
> How did you prove that no one could just put in an arbitrary integer into that function? Does it fail to compile? The answer quite literally follows immediately after the code sample you quoted: > Attempting to prove the absence of runtime errors gives us the following warnings: buffer_overflow.adb:162:26: medium: unexpected exception might be raised 162 | Ada.Integer_Text_IO.Get (Index_To_Clear); | ~~~~~~~~~~~~~~~…
To me, this doesn't sound like something unique to spark. Let's return to the solution example:
procedure Overflow_This_Buffer
with SPARK_Mode => On
is
type Integer_Array is array (Positive range ) of Integer;
Int_Array : Integer_Array (1 .. 10) := [others => 1];
Index_To_Clear : Integer := Int_Array'First - 1;
begin
while Index_To_Clear not in Int_Array'Range loop
Ada.Text_IO.Put ("What array index should be cleared? ");
-- Read the new array size from stdin.
Ada.Integer_Text_IO.Get (Index_To_Clear);
end loop;
Int_Array (Index_To_Clear) := 0;
end Overflow_This_Buffer;
> If we wrap the Get call in a loop, and poll the user continuously until we have a value within the array bounds, SPARK can actually prove that a buffer overflow can't occur. (Remember to initialise the Index_To_Clear variable to something outside this range!)
You have to poll the user continuously until a valid input is given. Again, I don't see how this is any different or special compared to any other programming language that would handle the error by asking the user to retry the function.
> Key word here is can. You can write correct software using any language, from raw binary to theorem proving languages, but some languages check more properties at compile time than others. What using something like SPARK/Lean/Agda/Rocq buys you is the "more" part, up to allowing you to eliminate runtime checks entirely because you proved at compile time that the corresponding error conditions can not happen (e.g., proving that indices are always in bounds allows you to omit bounds checks). That's not something the more popular languages are capable of because their type system is not expressive enough.
But I think the discussion here is about Rust, Ada, C/C++ no? The type system in Rust, Ada, and C++ are all robust enough at least to accomplish this.
> This seems contradictory, especially when considering that type checking is creating a formal proof?
Exactly! This is the root of my issue: you can accomplish this magical "proof" you speak of without using SPARK or Ada or any special "contract" language.