Great share thank you! There is incredible motivation for typed calculus
here: Where there are formal properties a proof may be pursued to build
reliable abstractions.
Where and how such methods are applied must still remain the purview of
thoughtful design.
Cheers,
Darren
On Jun 25, 2014 8:25 AM, "Francesco Ariis"
On Wed, Jun 25, 2014 at 02:45:37PM +0200, Mateusz Kowalczyk wrote:
While I disagree with initial view that testing is useless, I certainly disagree with this approach too. There are plenty proof-assistants using type-checking to prove programs correct. That's not to say Haskell itself is suited for such task. If you have a type system strong enough, classical tests are no longer required because you can encode all the properties you need in types proving at compile time that your program is in fact correct.
For non-believers, here is a blog post that opened my eyes on the matter [1].
[1] http://lambda.jstolarek.com/2013/12/data-is-evidence/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe