On 2008 Oct 19, at 11:24, Friedrich wrote:
"Brandon S. Allbery KF8NH" <allbery@ece.cmu.edu> writes:
The relationship between types and proofs is especially obvious in Haskell. And proofs aren't merely mathematical entities, they're expressions of what you want to accomplish: if you can type your program, you have a high likelihood not only that it will compile, but that it will do what you intend. Well I could argue with the types in C and would not come along very far. In the TCP/IP stuff one can see what you have to do, sooner or
From a Haskell standpoint, C and Java are virtually untyped. If you want to see types => programs in action, play around with the @free and @djinn commands in lambdabot (a Haskell bot that lives on FreeNode). @free treats a type as a theorem and produces a "proof" of it in Haskell code; @djinn takes a function declaration (type -> type) and generates the "obvious" code suggested by the declaration. (@djinn is sadly somewhat limited; it doesn't handle recursive types, so e.g. lists don't work too well.) -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH