So it seems that you can get pretty far with just type definitions as a formal model of a system. The typed properties verify that the properties will have that type, typed function arguments verify the functions will get the appropriate input and output types, etc.
But now I am wondering about algorithms. In an ideal world an algorithm would just be a typed object as well and the algorithm's correctness would be inherent in the type definitions. I can't see how that would be possible, so I resort back to my brief readings of proving algorithms. Essentially you want to have an assertion before and after any loop, to establish a loop invariant. This way you can reason through induction that every step of the algorithm works as expected.
I am just not sure what I want to prove in the first place. I would like to have my code be:
- Fault tolerant.
- All the things you would typically want.
So I define a specification for the algorithm:
- The algorithm should return a type x object (types handle it automatically).
- The algorithm should ~~ chug through the elements one at a time and compute a sum (lets say) ~~. That's where it starts to get fuzzy. Wondering if this is where the "loop invariant" comes in.
- If there are no loops or branching in the algorithm (but maybe if-statements), then I want to prove (or "validate") that the value falls within some set of acceptable values.
So it seems that the quality of the application is dependent on how well-specified the behavior is. If you miss edge-cases, there will be bugs. If you don't specify the acceptable output values of the function, then you may get XSS. Wondering if that is a correct assessment, that everything revolves around the specification. Without that, there is nothing to prove.
Then it seems that you need to do testing first, in order to even comprehend the types of things you want to prove to be correct. It's like you start with some unit tests, and slowly evolve it to proofs. Wondering if that is a correct assessment. Once you know all the inputs and outputs of the algorithm through some thorough testing, then you can write some sort of proof that the algorithm is correct and avoids the error cases. This just seems like a really good unit test.
To summarize, it seems like what you want to prove with algorithms is that they are correct with regards to a specification. And the specification is a living document that you can start out with by writing unit tests which slowly evolve into proofs (somehow).
Just looking for some pointers on if I am on the right track, and how to know what to prove in an algorithm.