Currently I am wondering how to apply proofs to web applications. So far it still isn't clear to me what a proof would look like for such a situation. I would like to see from a math perspective how to write a high level proof for something in the real world.
For example, say you are building a piece of software, whether it is a Computer Algebra System, a LaTeX parser, a graph visualizer, a scholarly paper hosting site, or all of the above. It is said that using formal methods it is possible to write proofs about this software and its adherence to a rigorous, formal specification, such as specified by Coq perhaps.
What I am missing is what this proof would look like, in rough sketch / natural language form. Just enough to get me started in seeing how proofs can come to life in the software world.
The best I can do so far in imagining something that might be provable, and what the proof looks like, is this. (I'm looking for an example that involves side effects using impure third party unverified stuff). Drawing a triangle on the screen. I can prove through evidence that this is true by demonstrating that it is true visually. By testing (i.e. "unit testing"). This might satisfy the more general definition of proof, but doesn't seem to satisfy the rigorous formal definition. So the question is if I can prove that it will draw to the screen without testing. That is where my mind draws a blank. I can't see how to prove that you can draw to the screen without unit testing. I am trying to think of an example where you could somehow say "since a and b, and b -> c, then c" or something. But there's a big gap there that I can't seem to close.
Wondering if you could sketch a rough proof of something about a software environment that involves unknowns and side effects, yet demonstrates a real thing that could really be proven (perhaps by using a specification). Something other than type theory, or the standard formal verification examples such as termination or completeness checking. Even if it is extremely complex.
Another attempt... So you have your base platform, and you create observations from it. These observations are confirmed by unit tests. From the unit tests we can get axioms. The axioms are then used to construct theorems. So you come up with a theorem from the axioms, like for all (x, y, z) tuples where x, y, z are integers, if you call foo(x, y, z) you will get a triangle. Or that would be the axiom actually. Another theorem might be.... Hmm... Not sure yet. But it seems if you could define some sort of theorems, then you could define a proof for that theorem.
Maybe this... If I also have an axiom for an array of bits encoded as utf-8 forms a string, then I can say the theorem is I can convert the string into integers, and so generate a set of triangles from the string by calling foo for each triple of characters.
Then the proof would be something like "assume foo, and assume a string, then by the property of strings converting to integers, we can create integers. then by the property of grouping we can group them into triples. thus we have triangles for every integer tuple."
Trying to find some way to connect the dots.