The Curry–Howard correspondence also raised new questions regarding the computational content of proof concepts which were not covered by the original works of Curry and Howard. In particular, classical logic has been shown to correspond to the ability to manipulate the continuation of programs and the symmetry of sequent calculus to express the duality between the two evaluation strategies known as call-by-name and call-by-value.

Speculatively, the Curry–Howard correspondence may be expected to lead to a substantial unification between mathematical logic and foundational computer science: …

— Wikipedia on Curry–Howard correspondence

2010.03.08 Monday ACHK

If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: a proof is a program, the formula it proves is a type for the program. Most informally, this can be seen as an analogy which states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.

The correspondence has been the starting point of a large spectrum of new research after its discovery, leading in particular to a new class of formal systems designed to act both as a proof system and as a typed functional programming language.

— Wikipedia on Curry–Howard correspondence

2010.03.07 Sunday ACHK

* Access to computers — and anything which might teach you something about the way the world works — should be unlimited and total. Always yield to the Hands-On Imperative!
Levy is recounting hackers’ abilities to learn and build upon pre-existing ideas and systems. He believes that access gives hackers the opportunity to take things apart, fix, or improve upon them and to learn and understand how they work. This gives them the knowledge to create new and even more interesting things (Levy, 1984:226). Access aids the expansion of technology.

* All information should be free.
Linking directly with access, information needs to be free for hackers to fix, improve, and reinvent systems. A free exchange of information allows for greater overall creativity. In the hacker viewpoint, any system could benefit from an easy flow of information.

* Mistrust authority — promote decentralization.
The best way to promote the free exchange of information is to have an open system that presents no boundaries between a hacker and his quest for knowledge. Hackers believe that bureaucracies, whether corporate, government, or university, are flawed systems.

* Hackers should be judged by their hacking, not criteria such as degrees, age, race, sex, or position.
Inherent in the hacker ethic is a meritocratic system where superficiality is disregarded in esteem of skill. Levy articulates that criteria such as age, sex, race, position, and qualification are deemed irrelevant within the hacker community. Hacker skill is the ultimate determinant of acceptance. Such a code within the hacker community fosters the advance of hacking and software development.

Testament to the hacker ethic of equal opportunity, L. Peter Deutsch, a twelve-year-old hacker, was accepted in the TX-0 community, though was not recognised by non-hacker graduate students.

* You can create art and beauty on a computer.
Hackers deeply appreciate innovative techniques which allow programs to perform complicated tasks with few instructions. A program’s code was considered to hold a beauty of its own, having been carefully composed and artfully arranged. Learning to create programs which used the least amount of space almost became a game between the early hackers.

* Computers can change your life for the better.

Hackers felt that computers had enriched their lives, given their lives focus, and made their lives adventurous. Hackers regarded computers as Aladdin’s lamps that they could control. They believed that everyone in society could benefit from experiencing such power and that if everyone could interact with computers in the way that hackers did, then the Hacker Ethic might spread through society and computers would improve the world. The hacker succeeded in turning dreams of endless possibilities into realities. The hackers primary object was to teach society that “the world opened up by the computer was a limitless one” (Levy 230:1984)

… free and open source software allows hackers to access the code used to create the software to improve or reuse it. In effect the free and open source software movements embody all of the hacker ethics.

— Wikipedia on Hacker ethic

.

“Hacker” here means a highly skilled programmer, not a computer criminal. — Me

The basic difference is this: hackers build things, crackers break them. — Eric S. Raymond

“In academia, a “hacker” is a person who follows a spirit of playful cleverness and enjoys programming.” -– Wikipedia on Hacker (academia)

.

.

2010.03.06 Saturday ACHK