Lambda the Ultimate

I just started reading "Type Theory and Functional Programming" and realised pretty rapidly that I wasn't sure what a proposition was.

When I look at Wikipedia - http://en.wikipedia.org/wiki/Proposition - they seemed rather negative on the whole idea. If propositions are questionable how can you do something as concrete as write programs with them?

Am I just getting two different meanings of "proposition" mixed up? In the article it says

In Aristotelian logic a proposition is a particular kind of sentence: one which affirms or denies a predicate of a subject.

Even I know what a predicate is, so should I just run with this definition?

Thanks.