Hacker News Reader

> 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);
        |      ~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~

  buffer_overflow.adb:164:18: medium: array index check might fail
    164 |      Int_Array (Index_To_Clear) := 0;
        |                 ^~~~~~~~~~~~~~
    reason for check: value must be a valid index into the array
    possible fix: postcondition of call at line 162 should mention Item 
    (for argument Index_To_Clear)
    162 |      Ada.Integer_Text_IO.Get (Index_To_Clear);
        |                         ^ here

> The SPARK prover correctly notices that there's nothing stopping us from entering a value outside the array bounds. It also points out that the Get call we're using to read the integer from stdin can raise an unexpected Constraint_Error at runtime if you type in anything that can't be parsed as an integer.

This is followed by a version of the program which SPARK accepts.

> Then you're just making a custom type which enforces valid state which, again can be done in any language with a rich type system and if statements.

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.

> Formal proofs make sense when you're trying to come up with new formulas or studying the cosmos, but they make no sense when you're trying to predict how bits will behave on a computer, because for the most part that is a solved problem by languages themselves.

This seems contradictory, especially when considering that type checking is creating a formal proof?

View on HN

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;