That's why I used phrase "working program" and "verified" in my comment. ;-) If you have a working (tested) program, you might not have a mathematical proof th

That's why I used phrase "working program" and "verified" in my comment. ;-) If you have a working (tested) program, you might not have a mathematical proof that it works, but you have certain sense that what you're doing is not entirely logically implausible. It is a form of verification (although without complete guarantee of correctness). (Another way to look at it is that the testing you did determines what kind of sentence you proved to be true. So instead of assigning the type to the program in advance, you deduce it the other way around - we observe how the program works and that gives us its type.)