the program-proof analogy
"claim" (How do you say "claim" in Coq?, i.e. an unproven starting point, usually used as a more readable compromise between forward- and backward-chaining) is analogous to a "macro let" (i.e. a 'let' that doesn't evaluate the init-values, but simply binds the declared symbols to code... what's the correct name for it?). In this analogy, a normal 'let' is a claim + proof (proof is evaluation).

Cut-elimination is analogous to macro-expanding this code: it's a way of getting a normal form for the proof/program (which may be interesting if you are interested in coding standards or in automatic programming). But it's a pretty stupid thing to do if you care about program-efficiency / proof-readability, since regular "let" stores the value of the computation (like memoizing), whereas "macro let" doesn't, and will compute the same value several times.