The first thing to realize is that if a programmer writes a program, he thinks it works. In other words he has an informal proof in his mind that the program displays some specific properties.
I wouldn’t call it “an informal proof” exactly but I agree what goes on in the mind minds of programmers—modeling, concept processing, pattern matching, simulation—is somewhat close to it.
The difficulty is getting this out and into the program. Types are what seems to have worked best so far to help with it but maybe something better can be found. Or better ways to infer and display types.
I think this is the key insight from this post:
I wouldn’t call it “an informal proof” exactly but I agree what goes on in the mind minds of programmers—modeling, concept processing, pattern matching, simulation—is somewhat close to it.
The difficulty is getting this out and into the program. Types are what seems to have worked best so far to help with it but maybe something better can be found. Or better ways to infer and display types.