> > Why do you arbitrarily require that theorem proving be > the > > only way to prove correctness? What reasons do you > have > > to reject FSV? > > > > I am not a specialist or a mathematician, but I hang out > long enough in LtU to learn to appreciate theorem proving. > I would like my software not to have any corner cases that > bugs might lurk in. Of course that's not entirely doable > with current technology...
Complete FSV proves all possible states are consistent with the specification. It is doable with currrent technology (as the article explains) but not for all applications. Probably very few at this point.
In any event, what I don't understand about your argument is that testing doesn't prove software correct (e.g. theorem proving) either. If you are going to reject static typing for this reason you should also reject testing. Clearly that's absurd so I would like to discuss the real reasons why you think static typing should not be used.
Previous Topic
