There is an interesting move underway by the US Securities and Exchange Commission (SEC) to more precisely define the meaning of certain asset backed securities (like the now infamous mortgage-backed securities that were central to the recent crash). The NY times has covered the story from a high level, but what of particular interest to me is the proposal to specify the meaning of the bonds in Python. This is a step is the right direction but Python is not the answer.
The core problem here is to give a clear and unambiguous meaning to a bond. This requires the language in which it is written is precisely defined. Python is not precisely defined. There is only a prose definition of the language, which is inadequate in the same way that the prose definitions of bonds are inadequate, and of course there are differences between various versions and implementation of Python. Since Python is not precisely defined the only meaning one can give to a program in Python is whatever the particular implementation one uses does with that program.
In contrast there are languages that are formally defined, such Standard ML and Scheme. These would make a sound basis for the formal definition of bonds. In turns out that functional languages also make a good (meaning expressive and convenient) basis for the formal definition of bonds. There is a great paper on expressing contracts in Haskell and at least one company has implemented this idea in a commercial system (in O’Caml, I believe). So my advice to the SEC: use an appropriate subset of Scheme or Standard ML, or hire someone to create a formally defined DSL, but don’t use a language without a formal definition if precision is your goal.
There are a few broken links above
Thanks, Ethan – corrected!
How strong is the case that Python should be avoided because it doesn’t have a formal definition? I ask because I’m considering whether SIGPLAN should register a formal reply to the SEC request for comments.
Haskell doesn’t have a formal definition. I suspect O’Caml does not either. SML does, but SML sees relatively little use these days. Scheme does, and is in wide use, but I’m unclear on how well the implementations adhere to the spec; my impression is that there are both R^5 and R^6 and other implementations in circulation.
Do you have evidence that Python implementations vary enough to cause errors when used for formal specification?
Do you have evidence that other languages do not vary in the same way?
Yours, — P
It seems somewhat unlikely that the kinds of ambiguities that programming language designers worry about would cause a significant problem with a financial contract. As long as the meaning of the arithmetic operators is well-understood and you have all the normal control-flow behavior, you’ll probably be OK. However, there is kind of a big hole in Python’s definition with respect to financial contracts: the precision of floats is implementation-defined and the precise meaning of floating-point operators is not specified—they are not guaranteed to have IEEE 754 semantics.
There’s a whole bunch of misunderstandings both in the post and in the comments:
- The right way to specify financial contracts isn’t with a general computer program: The idea that giving the user the ability to fiddle with inputs and observe variations in output is going to give better transparency. It’s true the fact that Python doesn’t have formal semantics makes *this* particular model useless or at least unenforceable – after all, the issuer’s Python might have different bugs than the customer’s. The formal semantics of Scheme or Standard ML would improve this aspect, but doesn’t change the fact that it’s the wrong model in the first place.
- MLFi’s contracts aren’t specified in O’Caml – instead, O’Caml programs are used to construct contracts, which are (or were, last time I looked) first-order data values. *These* need (and have) a formal semantics. So the way to go is to create a special DSL for financial contracts – then it does not matter so much what the software that manipulates it is written in.