I don't think it's a bad idea. It'd save everyone a lot of re-implementation, and the maths for the waterfall is likely to be clearer than the prose.

Not sure about Python. MatLab is the "industry standard" (ok, more people use Excel, but we don't want that) modelling tool. By far the best treatment of financial contract & programming I know of was in Haskell.
http://research.microsoft.com/en-us/um/people/simonpj/Papers/financial-contracts/contracts-icfp.htm

But you're right, it's the assets, not the waterfall, that were the issue. People didn't go out and check things in real-life - and there was no incentive to.

I have suggested trading at the level of individual mortgages, with tranches sliced through the mortgage itself, rather than a pool.
http://thomasbarker.com/content/orphaned-mortgage-article

For as long as banks are concentrating on gaming their capital requirements, and pension funds on minimising their contributions, there's no incentive to start doing things accurately.

"formal proofs of contracts are the domain of the courts, not compilers."

Of course the court's answers can differ from the computer's, and the court's are legally authoritative, but the same is true for courts and contracts vs. accountants and their spreadsheets. What is reported on a financial statement is an extreme simplification of what is actually in a company's contracts.

What the SEC seems to be trying to do, and what traders on Wall Street has been doing for many years, is to move beyond spreadsheets to summarize the value of contracts like derivatives, which can be highly inaccurate, to accountants and programmers using algorithms to summarize the value of these kinds of contracts, which can be far more accurate. Python makes for a great improvement for these purposes over the formulas in a spreadsheet, although my own contract language (or its successor in the works) would be better as unlike Python it easily models the temporal relations in a contract.

http://szabo.best.vwh.net/contractlanguage.html