> Let's keep things civilized, okay?

Formal verification of large, very complex real-world systems is what I do all day every day. If you don't understand what it is that I'm saying (and that's my fault -- I'm probably not clear enough) you can just ask. I'm a practitioner, not a theoretician, so I may make mistakes, but I think that in this particular case you are too attached to the typed LC to consider other reasoning systems (which, BTW, happen to be far more prevalent in the verification community).

> This doesn't even make sense. A program can be run. What does it mean to “run a proposition”?

Let's step back and consider the theory and then get to the specifics. Consider the set of all TMs (perhaps TMs isn't the best name because it may imply a specific programming model, but that is not my intent; I'm using the term here interchangeably with an abstract state machine, or a program). Each and every one of them is "runnable", right? Each and every subset of that set also consists of TMs, which are also runnable, right? A proposition about a TM constitutes such a subset. Under certain conditions, you can incorporate all DTMs in the set corresponding to the proposition into a single NDTM, which can also be run. Hence, there is a direct correspondence between propositions about programs (e.g., the program returns its input sorted) and NDTMs. Hence, you can most certainly run a proposition about programs (though perhaps not all propositions).

The temporal logic of actions (TLA) is a complete logic in the sense that for every NDTM (or a DTM as a special case) there exists a (non-unique) TLA expression, consisting of the simple logical connectives, the priming operator (an action) and possibly LTL operators (describing say, fairness, properties) that describes that particular TM. But, of course, a TLA expression can be less precise, and describe a whole set of TMs -- a proposition. Therefore in TLA, propositions and programs are the same object. Here's Lamport in the opening paragraph introducing TLA in the 1993 paper[1]:

Correctness of [an] algorithm means that the program satisfies a desired property. We propose a simpler approach in which both the algorithm and the property are specified by formulas in a single logic. Correctness of the algorithm means that the formula specifying the algorithm implies the formula specifying the property, where implies is ordinary logical implication.

FYI, that paper has 2458 citations and is far from obscure. This theory is much better known in the software verification community than type theory (certainly when you consider it within the greater framework of temporal logics, of which TLA is one), and has had a greater impact -- both academic and real-world -- on formal methods, at least so far. Specifying programs as propositions in temporal logics was a modern theoretical turning point in CS, and has yielded two or three Turing awards (Pnueli in '96, Clarke et al. in '07, and Lamport -- at least partly for this -- in '13).

> Even if I charitably interpret that as “decide its truth value”, well, not all propositions are decidable!

This is where things are a bit tricky. For a complete treatment see the preliminaries section in this '88 paper by Abadi and Lamport[2].

> A proposition has a truth value - a proof does not.

Of course, but there's room for interpretation here (like I said, I'm not a type expert so I'm not 100% sure about it): `<x = 3, y = 5>` can be viewed as a proof object of the proposition `∃x,y ∈ 1..10 . x < y`, but it can also be viewed as the more precise proposition, `x = 3 ∧ y = 5`. Existential propositions (or types) can therefore be viewed as a set of multiple programs, while the proof object is a particular program, that could have been specified with a more precise proposition. That is what I meant when I said "hidden proposition".

If you step back from typed LC and consider the original proof objects, those objects are just a series (a tree, actually) of logical deductions. Each of those deductions is a proposition. A proof is, therefore, a series of true propositions, each derived from the previous one using one of the deduction rules. You can certainly say, then, that a proof is a collection of hidden (true) propositions.

[1]: http://research.microsoft.com/pubs/64074/lamport-actions.pdf

[2]: http://research.microsoft.com/pubs/64046/abadi-existence.pdf