61–70 of 173 posts
I’m not really into languages like this. Anybody got some resources regarding how strict the guarantees can get in either of these types of environments?
Earlier quoted context omitted.
> These are subsets of their respective languages, but Pretty much every language has such a subset. Nothing new then, sigh...
C and C++ don't have such a subset. That seems pretty relevant, given they're the languages being compared and they're used for the majority of safety critical development. The standards I mentioned use tricks to get around this. MISRA, for example, has the infamous rule 1.3 that says "just don't do bad things". Actually following that or verifying compliance are problems left completely to the user. On the other han…
Taking this default is not enough to write safety-critical software… but it’s enough to write a browser (in theory) or some Android core daemons.
C++ is a good alternative to "C/C++"
Earlier quoted context omitted.
> 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…
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…
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
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?
Their example of why Ada has better strong typing than Rust is that you can have floats for miles and floats for kilometers and not get them mixed up. News flash, Rust has newtype structs, and you can also do basically the same thing in C++. I don't know much about Ada. Is its type system any better than Rust's?
Earlier quoted context omitted.
> 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…
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…
The idea is that you define a number of pre- and post- condition predicates for a function that you want proved (in what's effectively the header file of your Ada program). Like with tests, these checks that show that the output is correct are often shorter than the function body, as in this sorting example.
Then you implement your function body and the prover attempts to verify that your post-conditions hold given the pre-conditions. Along the way it tries to check other stuff like overflows, whether the pre- and post- conditions of the routines called inside are satisfied, etc. So you can use the prover to try to ensure in compile-time that any properties that you care about in your program are satisfied that you may otherwise catch in run-time via assertions.
Earlier quoted context omitted.
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 si…
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.
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.
Earlier quoted context omitted.
> These are subsets of their respective languages, but Pretty much every language has such a subset. Nothing new then, sigh...
C and C++ don't have such a subset. That seems pretty relevant, given they're the languages being compared and they're used for the majority of safety critical development. The standards I mentioned use tricks to get around this. MISRA, for example, has the infamous rule 1.3 that says "just don't do bad things". Actually following that or verifying compliance are problems left completely to the user. On the other han…
I know there is a belief that Rust/Ada etc is safer than C/C++ and in some cases that is true. I know of multiple, airworthy aircraft that are flying with C++ code. I also know of aircraft flying with Ada. The aircraft flying with Ada is hard to maintain. There is also a mountain of testing that goes into it that is not just unit testing. This mountain of integration, subsystem and system level testing is required re…
What makes Ada harder to maintain? Do you have a source for that so I could read more?
Continuity: Ada is not widely taught at universities, and, whilst the AdaCore’s GNAT Academic Program (GAP) does exist, one has to consciously seek out a university that offers a course in/on Ada. Ada and programming in Ada is not common knowledge, which stems from the next point.
PR. Ada, rightfully or wrongully, does not exactly bask in the limelight of popularity – most assuredly not to the same extent as Python, NodeJs, Typescript, C#/.NET etc do. The current generation of Ada developers do not care (and probably should not), and the young and future generations of potential Ada developers miss out. Ada is not talked about in diverse contexts spanning web development, frontend/backend[0] development, containers, cloud – and the list goes on. Not because Ada can't be used in any of the aforementioned contexts, it is just that due to the lack of PR it remains an unnoticed reality – kind of like «if a tree falls in a forest and no one is around to hear it, does it make a sound?»
[0] Yes, «frontend development» and «backend development» are the fancy terms in wide use that the new generation can easily understand.