Yes, types are proofs, so it's possible for statically typed code to have no tests and be proven to be correct. Also, tests can't prove anything correct unless they're exhaustive. Practically, it's a continuum, so there are more things you need to test in Java than in Haskell, and the compiler does the whole job itself in Agda. In fact, a couple of days ago I wrote a subtract function in Agda, calls to which *won't compile* if it would yield a negative number. Not for any real purpose, just trying to expand the old mind.
I'm not even sure if I could write a unit test for that, as the failure cases wouldn't compile. On Tue, Jul 31, 2012 at 4:23 AM, Russel Winder <[email protected]> wrote: > On Mon, 2012-07-30 at 10:41 +0100, Kevin Wright wrote: > > Unit testing *cannot* prove correctness by itself, try this for a thought > > experiment: > > This argument is only really useful in this debate if statically typed > codes need no unit tests at all in order to provably correct. Reality is > that all codes need to have unit, integration and system tests, so the > above becomes just a truth for all software development. > > -- > Russel. > > ============================================================================= > Dr Russel Winder t: +44 20 7585 2200 voip: > sip:[email protected] > 41 Buckmaster Road m: +44 7770 465 077 xmpp: [email protected] > London SW11 1EN, UK w: www.russel.org.uk skype: russel_winder > -- You received this message because you are subscribed to the Google Groups "Java Posse" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/javaposse?hl=en.
