5 ms·

> Regardless of the language, you cannot write some special program that guarantees an input will be valid if it comes from an external source or a human. It is

by ajxs 1y ago

> Regardless of the language, you cannot write some special program that guarantees an input will be valid if it comes from an external source or a human. It is simply impossible to prove this at compile time. > ...but from my perspective it looks worse in Ada... This isn't really true. SPARK obviously can't prove that the input will be valid, but it can formally prove that the validity of the user input is verified before it's used. I wrote about this here: https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Against_Rust.html#buffer_overflow https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Aga...

vouwfietsman 1y ago
I am no expert here what I remember is mostly from CS courses, but isn't the entire point of a formal program proof that you can reason about the combinatorics of all data and validate hypothesis on those? It's one thing to say: "objects of this type never have value X for field Y", or "this function only works on type U and V", but its a lot more impressive to say "in this program state X and Y are never achieved simultaneously" or "in this program state X is always followed by state Y". This is super useful for safety systems, because you can express safety in these kinds of functions that are falsifiable by the proof system. E.g: "the ejection seat is only engaged after the cockpit window is ejected" or "if the water level exceeds X the pump is always active within 1 minute".
- waterTanuki 1y ago
  But isn't the entire point of rust's verbose type system to declare valid states at compile time? I don't exactly see how this can't be proved in rust.
  - aw1621107 1y ago
    > But isn't the entire point of rust's verbose type system to declare valid states at compile time? Different type systems are capable of expressing different valid states with different levels of expressivity at compile time. Rust could originally express constraints that SPARK couldn't and vice-versa, and the two continue to gain new capabilities. I think in this specific example it's possible to write a Rust program that can be (almost) verified at compile time, but doing so would be rather awkward in comparison (e.g., custom array type that implements Index for a custom bounded integer type, etc.). The main hole I can think of is the runtime check that the index is in bounds since that's not a first-class concept in the Rust type system. Easy to get right in this specific instance, but I could imagine potentially tripping up in more complex programs.
  - vouwfietsman 1y ago
    I am not a Rust expert either, but just a general remark: using a programming language like Rust as its intended to be used, i.e. functional/imperative programming of the problem domain, does not lend itself well to proving/disproving the kind of statements I showed above. Yes, you could theoretically generate a Rust program that does not compile if some theorem does not hold, but this is often times (unless the theorem is about types) not a straightforward Rust program for the problem at hand. I also think that, although Rust is blurring the lines a bit, equating formal verification and type-checking is not a valid stance. A type checker is a specific kind of formal verification that can operate on a program, but it will only ever verify a subset of all hypotheses: those about object types.
- ajxs 1y ago
  > isn't the entire point of a formal program proof that you can reason about the combinatorics of all data and validate hypothesis on those? You're right. Validating input is a part of this process. The compiler can trivially disprove that the array can be safely indexed by the full set of any valid integer that the user can input. Adding a runtime check to ensure we have a valid index isn't a very impressive use of formal proofs, I admit. It's just a simple example that clearly demonstrates how SPARK can prove 'memory-safety' properties.
waterTanuki 1y ago
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_This_Buffer; What I am asking is what exactly is formally proving from 1st principles? Because to me this looks no different than a simple assertion statement or runtime bounds check which can be performed in any language with if statements & exceptions. How did you prove that no one could just put in an arbitrary integer into that function? Does it fail to compile? 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. If I might be more blunt: formal proofs in the field of programming appear to be nothing more than mathematicians trying to strong-arm their way into the industry where they aren't necessarily needed. 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.
- aw1621107 1y ago
  > 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?

by ajxs 1y ago

vouwfietsman 1y ago

I am no expert here what I remember is mostly from CS courses, but isn't the entire point of a formal program proof that you can reason about the combinatorics of all data and validate hypothesis on those? It's one thing to say: "objects of this type never have value X for field Y", or "this function only works on type U and V", but its a lot more impressive to say "in this program state X and Y are never achieved simultaneously" or "in this program state X is always followed by state Y". This is super useful for safety systems, because you can express safety in these kinds of functions that are falsifiable by the proof system. E.g: "the ejection seat is only engaged after the cockpit window is ejected" or "if the water level exceeds X the pump is always active within 1 minute".

waterTanuki 1y ago
But isn't the entire point of rust's verbose type system to declare valid states at compile time? I don't exactly see how this can't be proved in rust.
- aw1621107 1y ago
  > But isn't the entire point of rust's verbose type system to declare valid states at compile time? Different type systems are capable of expressing different valid states with different levels of expressivity at compile time. Rust could originally express constraints that SPARK couldn't and vice-versa, and the two continue to gain new capabilities. I think in this specific example it's possible to write a Rust program that can be (almost) verified at compile time, but doing so would be rather awkward in comparison (e.g., custom array type that implements Index for a custom bounded integer type, etc.). The main hole I can think of is the runtime check that the index is in bounds since that's not a first-class concept in the Rust type system. Easy to get right in this specific instance, but I could imagine potentially tripping up in more complex programs.
- vouwfietsman 1y ago
  I am not a Rust expert either, but just a general remark: using a programming language like Rust as its intended to be used, i.e. functional/imperative programming of the problem domain, does not lend itself well to proving/disproving the kind of statements I showed above. Yes, you could theoretically generate a Rust program that does not compile if some theorem does not hold, but this is often times (unless the theorem is about types) not a straightforward Rust program for the problem at hand. I also think that, although Rust is blurring the lines a bit, equating formal verification and type-checking is not a valid stance. A type checker is a specific kind of formal verification that can operate on a program, but it will only ever verify a subset of all hypotheses: those about object types.
ajxs 1y ago
> isn't the entire point of a formal program proof that you can reason about the combinatorics of all data and validate hypothesis on those? You're right. Validating input is a part of this process. The compiler can trivially disprove that the array can be safely indexed by the full set of any valid integer that the user can input. Adding a runtime check to ensure we have a valid index isn't a very impressive use of formal proofs, I admit. It's just a simple example that clearly demonstrates how SPARK can prove 'memory-safety' properties.

waterTanuki 1y ago

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_This_Buffer; What I am asking is what exactly is formally proving from 1st principles? Because to me this looks no different than a simple assertion statement or runtime bounds check which can be performed in any language with if statements & exceptions. How did you prove that no one could just put in an arbitrary integer into that function? Does it fail to compile? 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. If I might be more blunt: formal proofs in the field of programming appear to be nothing more than mathematicians trying to strong-arm their way into the industry where they aren't necessarily needed. 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.

aw1621107 1y ago
> 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?