Lambda the Ultimate

Services like this are highly purchasable.

what the SEC is after, that is a formal definition of a bond. In fact, unless I'm reading this wrong, it's not even about defining precisely what a bond *is*, but about the rules that govern transactions.

To me it would seem that they want an algorithmic (and hopefully easy to read) representation of those rules, not a formal model of a bond to be verified against some type of formal specification.

If that's what is the former (and if the intended audience are traders and application programmers), then Python would be an excellent choice (certainly better than legalese English.) If it is the later, then I'd agree with you in that it cannot be achieved without a formal specification language.

In fact, were they to come up with *some type* of restricted subset of Python (both in syntax and programming style), they might be able to go formal-methods-light and have something readable by traders, something that can be reasoned, albeit in an informal manner.

That's better than plain ol' courtroom English (and can pave the way to further and future refinements and formalizations is there ever a need for them.)

But how do you know what a bunch of Python code means, algorithmically? And what is the source of that meaning?

Without a formal specification, the only way to conclusively interpret the meaning of a fragment of Python is by describing what happens if you run it on a particular implementation and a particular machine.

Say that someone files a program that does what they intend on version X of Python, Guido later releases version Y, the government is using version Z, and, for the sake of argument, that all three give different results. How would that be handled?

Of course that sounds unlikely, but consider that there will be a lot of smart people looking at the system, able and willing to take advantage of ambiguities if it benefits them.

It will mean what it will mean (ducks for cover:). They are not trying to get some sort of formal semantics for it. They are not looking for precision, but readability.

Look at it from the point of view of a reader, a trader or an applications programmer looking at a piece of code. That's the intended view. Assuming the code is well-written, that is the type of meaning that they intend to get. We know what a bunch of well-structured control structures (ifs and loops) mean.

They are not looking for a formal and precise meaning, but a pedestrian meaning, something that is cost-effective in removing a lot of ambiguity and verbosity from obscurantist English text.

I'd add at this point that there should be some sort of coding guidelines that'd govern how they'll use Python for this. It's not going to be a free-for-all wild west coding hackery either.

Some (if not most) of these rules and conditions that govern transactions are for the most part conditional statements amenable to be described tersely , without the verbosity inherent in legal documents. The SEC's objective is accessibility, not verifiability.

Also, the SEC doesn't necessarily concern itself about the absolute removal of all loop holes, but instead to presenting something readable so as to be interpreted in a manner of good faith. Loop holes and ambiguities are ironed out via revisions to the rules, and criminal exploits (not accidental) are simply prosecuted.

And given the legal context of these procedures, there will be things that will require legal interpretation and arbitration (and subsequent amendment.)

As for the hypothetical scenario of running something on multiple versions of Python, again, look at it from what these rules are: a bunch of if-statements, loops and perhaps some procedure calls with simple arguments. Are we to expect such basal things to realistically vary in their meaning from one version to another? Do we have evidence to suggest there is a probability sufficiently high to make that a concern?

To put it simply, the SEC is trying to present their guidelines as pseudo-code written in Python. And for most cases, pseudo-code just works fine. If the guidelines have an error, that's an error in the requirements. No amount of formalism can prevent that.

And, to reiterate, I don't think the SEC is looking for a formal specs from which to create a model that can be formally verified either. The intention is very different and does not warrant that type/depth of formalism.

Not everything warrants formalization.

You're quite correct, from a broad perspective. Doubtless even outright pseudo-code would be an improvement over an English description, and executable Python better still. If the code is unclear, that can be handled just as well as if a description in English were such.

It's just that, from the perspective of someone who thinks about programming languages, it seems odd to go as far as using an actual programming language yet not choose one that has an explicit and rigorous formal semantics.

Given that there's some history of financial institutions using ML-family languages, and that--if memory serves me--SML has a formal semantics, that would have seemed the obvious choice.

Imagine a hash table in your mind, with keys corresponding to every particular combinations of phonemes. Back up a second, instead of phonemes, let's just call them strings of characters, and imagine that we have no such thing as an auditory cortex.

In this hash table we look up the term "bond" and we get a bucket full of collisions.

Information floats into our consciousness...

chemical bond: an electrical force linking atoms
a certificate of debt (usually interest-bearing or discounted) that is issued by a government or corporation in order to raise money; the issuer is required to pay a fixed sum annually until maturity and then a fixed sum to repay the principal
alliance: a connection based on kinship or marriage or common interest; "the shifting alliances within a large family"; "their friendship constitutes a powerful bond between them"
bail: (criminal law) money that must be forfeited by the bondsman if an accused person fails to appear in court for trial; "the judge set bail at $10,000"; "a $10,000 bond was furnished by an alderman"
shackle: a restraint that confines or restricts freedom (especially something used to tie down or restrain a prisoner)
attachment: a connection that fastens things together
adhere: stick to firmly; "Will this wallpaper adhere to the wall?"
a superior quality of strong durable white writing paper; originally made for printing documents
bind: create social or emotional ties; "The grandparents want to bond with the child"
United States civil rights leader who was elected to the legislature in Georgia but was barred from taking his seat because he opposed the Vietnam War (born 1940)
issue bonds on
British secret operative 007 in novels by Ian Fleming
bring together in a common cause or emotion; "The death of their child had drawn them together"
adhesiveness: the property of sticking together (as of glue and wood) or the joining of surfaces of different composition; "the mutual adhesiveness of cells"; "a heated hydraulic press was required for adhesion"
wordnetweb.princeton.edu/perl/webwn

We quickly sort these definitions according to relevance, relying upon the old common law definition of "logical relevance" which relates to the phrase "tends to prove or disprove a fact of consequence [to the outcome of the litigation]."

We flip the contexts back and forth, and attempt to construe as much ambiguity as possible, see how we can evade liability. Is there any way to argue a mutual mistake of fact? A unilateral mistake of fact? We intentionally broadcast misunderstandings of the source's referential intention to the source, updating our model as the source provides us with clarifications. A unity of intent is achieved when only one possible set of contingencies is identified, and represented in terms of tarkian truth tables or something that a church-turing algorithm would understand.

No more slingshot arguments, no more reverse anchoring, no more little green pieces of paper, no more quack job 'n dakota house, all we wanna do is to make you bounce...

This message brought to you by the committee to return Ishtar's clothes to her, and the Dolphin Society for the preservation of the human species. s/quack/job

You're taking it to a whole new level, I guess. Good luck with that.

Having given this a couple of days more thought, the cheapest way to solve this problem is with the creation of a de-facto standard DSL for specifying contracts, which will then be used to load a generic Python harness (either via interpretation, code-generation, or just somehow including the DSL inline). Because of the size of the domain of financial contracts (10s of combinators over a base of at worst 100s of primitive values), this sort of problem is small enough to be solvable, but big enough to be profitably worth solving. The DSL could easily have purely declarative formal semantics while being programmer-readable.

However imprecise the Python semantics may be, they are much more precise than the current natural-language distinctions. Don't get so caught up in the PL viewpoint that you lose sight of the value of incremental advance.

I too think that Standard ML or Scheme would be a substantially better choice than Python, but even Python would definitely be a major step forward.

I am having a hard time deciding if people on Wall Street are lazy or eager. Surely, that's the way to decide which language they should use...

Chuck Prince, July 2007:

When the music stops, in terms of liquidity, things will be complicated. But as long as the music is playing, you’ve got to get up and dance. We’re still dancing.

That sounds eager to me, trying to obtain your return values regardless of whether you can terminate your long-term strategy. But maybe the financiers have changed.

Contracts are lazy in that they have an eventual value that in many cases won't be known until they're liquidated, i.e. until the thunk is forced. Before that time, though, they're assigned a speculative value, which is beyond eager: it's arriving at a value without actually evaluating (well, actually by evaluating something different, such as the optimism of the buyer.)

When a contract is liquidated, it involves a kind of backtracking: the final value has to be propagated through the system, affecting all the contracts that had previously been valued based on the underlying contract's speculative value.

In other words, to understand Wall Street, you need to understand continuations.

All people are lazy, but very eager when evaluated.

Nice.

People on wall street are lazy and greedy.

I don't see switching from Python to SML or Scheme as being difficult. It's not like there is already a body of Python code performing this task, and I don't think SML or Scheme is hard to learn (but of course I'm biased by the fact I've learned them).

... because it requires training a generation of programmers. It's noteworthy that one reason cited by Jane Street for why they love O'Caml is the impact it has on interviewing. They note that while the community that knows O'Caml is small, it's two sigmas above the norm, and this saves them the hassle of filtering out the glue coders. The mere fact that someone actually grasps O'Caml is a significant pre-filter.

But the corollary to that is that the pool of talent just isn't big enough (today) to support the type of wide use that is needed for something like automating contracts at scale.

From Jane Street Curriculum

Senior traders teach weekly finance theory classes on a wide variety of subjects, from highly practical subjects to abstract research topics.

Recently, some of our class topics have included:

* Introduction to Financial Instruments
* Futures and Commodities Arbitrage
* Options Valuation
* Portfolio Theory
* Bootstrapping the Yield Curve
* Visual Basic (VBA) for Beginners
* The Kelly Criterion
* Game Theory
* Decision Theory and Cognitive Biases
* Thinking About Extreme Risk and Derivative Valuation

Seems like OCaml isn't the only language they use. But I don't want to irritate your romanticisms.

Given the amount of spreadsheet use among non-programmers in a financial setting, I'd be more than a little surprised if they didn't use VBA. It would be like a web development outfit never touching Javascript.

You sometimes find success stories promoted by enthusiasts about the use of exotic languages in big financial companies like the one by shap or Haskell on Credit Suisse. When taking a closer look they aren't used there all that much and when you scan job offers other more familiar languages are demanded.

The statements I paraphrased originated with one of the Jane Street partners. I'm not saying that everyone there uses O'Caml. I very much doubt it. I know that the programmed trading group uses it heavily.

For the record, I'm decidedly not an O'Caml advocate. And you seem to have missed my point entirely, which was: even if a large company wanted to switch from Python to (e.g.) O'Caml, the cost of doing so is quite overwhelming. Noel's post suggested that he didn't understand this. I point to Jane Street not as an example of the success of O'Caml, but as an example of success derived from cornering the buyer's market on a critical skill base.

While Jane Street gains value from O'Caml, I think the main value they gain is its use as a filter for hiring purposes. Some people here cast that as a language success, and the two are hard to separate. I personally think it's a case of a useful correlated filter.

So don't let the primary sources hit you in the anti-romanticism on the way out, and perhaps next time actually read what you critique before you jump on the author.

This would be the same community that brought us CDOs and CDSs and whose software models led the world into one of the biggest economic catastrophes ever seen. And none of them foresaw this possibility.

I think next time I'll take developers a couple of sigmas down, please.

If academics were not arrogant hardly anyone would even notice them.

Arrogance might not be the most sympathetic character trait but it is surely a relevant social force and doing some useless stuff or learning about technology that no one applies is the price for being considered smart in some circles and therefore you get shielded by sneering remarks from respected colleagues who believe that most other human beings have an IQ just slightly above that of chimpanzees.

In every relationship there is an ironical reversion that subverts all good intentions. So what if the sigma++ people are trapped by the companies reputation of filtering only high potentials and using OCaml, Haskell or what not but precisely end up as those disdained "glue coders" and Excel sheet extractors? I love the stories of Google employees who have gone through the torture of 8 job interviews just to convert MS Word documents in the Googleplex, the temple of smarties. I read this sort of stuff and enjoy it when I recover from reading worthless papers about minimal, perfect hashtables that I intent to use as an optimization technique for an embedded OS I work out with my colleagues for an unpretentious Swiss company.

The reverse is not always true.

...managed to do that!? Wow, I had no idea.

Nope. The folks who brought you CDOs and bad models didn't work for Jane Street. They worked for Lehman, and Bear, and a few others. So those "couple of sigmas down" programmers are actually the ones who made the mess.

What information do you have about financial companies, and Jane Street in particular, that would cause you to make a statement like this? I hope it's more than an article in the Monad.Reader and the fact that Jane Street likes O'Caml.

And why exactly would you say "those [flame removed] programmers are actually the ones who made the mess"? What part do you believe that programmers played in creating CDOs and other financial contracts?

this article is fun.

The assumption that you need to be an ML (or Haskell or whatever) programmer to benefit from such frameworks seems wrong to me: a DSL or a GUI or both can shield most users from the implementation. For instance LexiFi has very complete .NET bindings as well as an elaborate GUI for its product and I gather that they are both very much used. See, e.g., the use cases on their web site.

In any case the SEC proposal seems geared more towards the executability of what-if scenarios (see 2nd paragraph of the quote on Pr Varma's blog), i.e., to clarify any questions interested parties might have which might affect profitability or risk assessment (their own or that of other parties), than towards specification per se. Thus you could conceivably take the view that the provided program, bugs and all, is the model: that is how a plain english contract functions. Not a sophisticated formalization but probably adequate for the purpose. This makes the choice of language a bit of a side-issue and we should be careful not to project our pet CS issues, interesting though they may be, onto the SEC.

Where difficulties could arise, IMO, is if a filing contains both code and plain english specifications: discrepancies between the two (inadvertent or deliberate) would inevitably creep in in many cases and then the parties and their lawyers would have a ball. That is a worse danger than ambiguities arising from the program itself but that is also not a programming issue and I think Ehud wants us to stick to that.

The always entertaining but often insightful Ian Grigg has just blogged on this, too, and he agrees with me that this is not about specification per se. You will note that he is in any case opposed to the very notion of formal specs (in the CS sense) for bonds or at least of such specs being given a legal standing. His attitude: that this is the domain of the courts, not of those meddlesome and delusional programmers and computer scientists, gives a foretaste of how the proposal will be met in some quarters. He has inveighed about this before, if memory serves me right, but I can't dig up the exact reference(s). They are likely to be a little offensive to this audience anyway.

About my concern expressed in the 3rd paragraph, I have since become aware of this sentence in §B.2, p.219: "We note that the waterfall computer program and the narrative description of the waterfall would need to be accurate and the accuracy of one would not compensate for inaccuracies in the other.", i.e., (if I read this correctly) exactly what I was afraid of. This is germane to this discussion because it is another strike against the notion that the program is meant to be the contract's spec.: if it were so, then it would make little sense to give it equal or subordinate status to the legalese description.

Unformal, semi-formal, or fully-formal, contracts are in the domain of courts, whatever you do. But the more formal, the less courts you need for a contract's concrete interpretation.

"We note that the waterfall computer program and the narrative description of the waterfall would need to be accurate and the accuracy of one would not compensate for inaccuracies in the other."

I read it differently. But it is Banker's Ballet, everyone is wearing their respective tutus. The public demands clarity, it will arrive, and Python's role will probably be short-lived. I.e., the direction will be towards formalization (possibly, of Python), or it will be abandoned in a few years.

Not so fast. There is a well-established precedent on Wall Street for going outside the court system: scores of contracts (such as those employees must sign) contain a mandatory arbitration clause that deprives you of recourse in the "normal" court system; instead your complaint is heard by an arbitrator, effectively a privately run parallel justice system. Wall Street is not the only but is a major user of this system, which is hardly a footnote or a curiosity. This is obviously a slippery slope and who is to say that it would not be conceivable, if the parties found it expedient, to give a computer program similar arbitration powers, thereby taking the courts entirely out of the loop?

I think people like you and Ian Grigg are being much too definite. How much scope there is for formal contracts in finance is more likely entirely up to the players.

A few points:

1. If you disagree with an arbitrator, you can always go to court. You can always fight a contract. At least, I hope it works that way in most countries.

2. The legal system is a sociological construct, so are arbitrators. We put our trust in courts as a medium for the public's 'feeling' of justice. Similarly, you can put your trust in arbitrators in case all parties agree; personally, I wouldn't, unless the option would be that you still can go to court. But neither system is perfect, and to some extend, this is irrelevant to this discussion too. (Actually, arbitrators in the financial world makes me wonder about the amount of closed-room deals going on.)

3. No-one in their right mind will assign arbitration powers on humans to a computer program. It is up to court to place a verdict on, for example, ownership of goods or bankruptcy. But you can formalize, to some extend, the ramifications.

How much scope there is for formal contracts in finance is more likely entirely up to the players.

I am not that definite on it. My personal view on the proposal is: Time is ripe, there is a window of opportunity, and it's worth a try. No-one can predict whether it will work. Maybe it will be abandoned in a few years, maybe it will work well and incur financial stability, maybe we create a new generation of cyber-bankers.

(What is the alternative? Have all financial tools first be scrutinized by a judge or government? Have the government mandate a fixed collection of financial contracts?)

[ And, another reason. As long as history goes, it has been proven on countless occasions that clear and open systems are the only sustainable ones, lest there be corruption and injustice. ]

Discussion of these topics is, of course, not on topic here.

While it is true that Python has no official formal semantics, its semantics are quite well understood. Most likely because it is not a particularly innovative language.

I would like to add that there is at least one inofficial formal semantics for Python which happens to be executable and written in Haskell. Disclaimer: I wrote it.

How about we take 2,000 children, 200 from each of the following age groups: 0.0-1.0 yrs, 1.1-2.0 yrs, 2.1-3.0 yrs ... N-N+.9 yrs.

We ask each of these children to specify with precision what bond means.

We make cross cultural comparisons between children who have never heard that particular combinations of phonemes before, and children who have been taught the entire entymology of the word by proto-indo-european professors, chinese professors, and any other linguist or academian or quack who wants to influence the child concerning the meaning of the word "bond."

We get responses from all these 2,000 children concerning a single query: "What does 'Bond' mean?"

These responses are recorded and the recordings are translated into strings of characters that are stored as private variables attached to vertices, one vertex per child.

We then write an algorithm that searches for overlap or common referents used in similar senses among the various private data structures associated with each of the nodes in this structure containing the 2,000 vertices corresponding to each child that has cast a vote.

Then we don't finish running this process, we leave it incomplete, and we never bother to define what a bond is, we leave ourselves in a state of mysteries, uncertainties, doubts, without any irritable reaching after fact or reason.

Per your suggestion, I promoted the story to the homepage.

Richard Gabriel commented on the question whether SIGPLAN should respond or not on Wadler's blog. I repeat the comment here because I think this is important:

'SIGPLAN should be neither an advocate nor detractor of any programming language. SIGPLAN's charter states:

"...SIGPLAN explores the design, implementation, theory, and efficient use of programming languages and associated tools." It is not an advocacy group.

It would be proper for SIGPLAN to put forth some considerations to keep in mind for an organization endeavoring to adopt a programming language for some purpose, but to suggest one or to recommend against another would seem to me to drop SIGPLAN (and by implication, ACM) into the realm of politics, or perhaps propaganda. That is, SIGPLAN should teach and little else in matters like this.'

to suggest one or to recommend against another would seem to me to drop SIGPLAN (and by implication, ACM) into the realm of politics

The ACM has a US-specific division that does get involved in politics to some extent, USACM.

(Although I agree that advocating a particular language would seem inappropriate for SIGPLAN.)

[ Great, I am replying to my own posts. ]

This smells like politics, not PLT. Feels like someone is pushing for financial clarity, fast. So let them write Python for a while, and formalize a Python-like Xml/DSL financial standard.

I might be wrong.

[ It depends on how far parties want to take the formalization serious, and what the end-goal is. But as a (fast) start, yeah. ]

[ Nah, sure of it. They just bypassed the standardization committee process which gives a lot of hassle, a 60-80% chance of success, and a two to four year time-frame minimal, to do it now while there's still commitment and people really want results, and they can push it through. ]

I take issue with a few of your bullet points.

Python
...
1. OO so (good) design
...
6. Probably doesn't scale because of high risk of spaghetti

While OO may very well be a way to write somewhat organized spaghetti code (paraphrased, I forgot the original quote and author). That doesn't seem like good design to me. Besides, good design does not stem from the language being used.

Haskell

1. FP so once specified, no real reason to expect logical errors

I love haskell but...

While it's true that haskell's compiler have helped me catch logical errors at times due to type errors that come out of my bad logic; I certainly wouldn't make a claim that strong.

3. Gives a formal specification

How so? Or more importantly, how does Python not give just as good of a formal specification? While any programming language does in some sense do this, and some may be closer than others, it doesn't make up for a real specification. Later in your post you say

3. Unreadable for people not used to FP, that includes the formal spec

Which hints at this.

1. Even with an expected easy problem domain, slow development cycle

My experience has been quite the opposite. Sure there was a learning curve for a while, and it may take more time per LOC. But I usually end up with smaller cleaner code and spend a lot less time debugging due to silly errors (type mistakes). I'd say (conjecture, but with a fair amount of experience in both languages) that I spend about 1/2 of the time solving a problem in Haskell than in Python. That includes time for development and testing.

2. Takes ages to hack new applications, poor integration with other tools

On the tools front, take a look at Visual Haskell. I haven't used it personally, but I would say that integration with VS is definitely a plus for those that prefer IDEs and the tools that come with them.

Hmm, all-in-all, except for the poor integration, and value-safety, Python isn't even a bad choice as a prototyping tool.

[ After some thought. It's a bad idea. Sure you can use Python a few years, but Python -or any other GPL- as a specification language? No, it should be formalized in a DSL/XML, possibly with a human readable front-end through XSLT. ]

I would choose Haskell, but I'm admittedly biased because I like it so much :). I'm sure Python could do the job as well and would be easier to find developers for. I certainly would not go with Java/XML/C#. I agree that a DSL is probably the best solution, but XML DSL's are terrible. Besides, DSLs are just so easy to implement in Haskell...

How many programs by how many programmers are that? What is the percentage of pure FP programmers in the US of all programmers, and how much time does it take to teach them?

I have taught Haskell. I shifted from Clean because of its interactive interpreter. 80% of those programmers, which was on a Hogeschool/ Fachhochschule/ College / University-of-Professional-Education got it to the point that they could solve simple problems. You need academics of reasonable quality to program in Haskell, and those who can, should be in design/middle-management in industry. Not code-monkeys.

I taught Python too. The difference between Python and Haskell, is that Python goes well with almost all programmers who are used to solving mediocre problems by writing a few lines, then running the program, and then adapting that. Python, by being untyped, even allows for substantial parts of the program not being specified and still to be run. (A do /think /do /think /do /think cycle).

Haskell, even with an interactive mode, is think-a-lot then do (think/ think/ think/ think/ do/ do). Haskell even punishes those who have mediocre designing skills, that would be around 60% of CS students. Only the top 3% in the field can be trusted with it.

For financial contracts, Haskell is pure overkill (pun intended).

Then to your points:

While OO may very well be a way to write somewhat organized spaghetti code (paraphrased, I forgot the original quote and author). That doesn't seem like good design to me. Besides, good design does not stem from the language being used.

Different points, OO doesn't lead to spaghetti code. Python is an OO, but also a dynamic, language. OO is (mostly) fine, but known to fail at points. Dynamic languages allow for free-style hacking. Unless you constrain that, you'll end up with spaghetti code.

While it's true that haskell's compiler have helped me catch logical errors at times due to type errors that come out of my bad logic; I certainly wouldn't make a claim that strong.

I think a claim: Once a proper Haskell program has been written (well) it holds little bugs, is valid. It's not only types, recursion and easily verified invariants play a role too.

How so? Or more importantly, how does Python not give just as good of a formal specification? While any programming language does in some sense do this, and some may be closer than others, it doesn't make up for a real specification. Later in your post you say

Ok, I don't even agree fully with myself here. Especially if the code is written in pure imperative monadic style, it doesn't. But, you can get pretty close for industrial standards.

My experience has been quite the opposite. Sure there was a learning curve for a while, and it may take more time per LOC. But I usually end up with smaller cleaner code and spend a lot less time debugging due to silly errors (type mistakes). I'd say (conjecture, but with a fair amount of experience in both languages) that I spend about 1/2 of the time solving a problem in Haskell than in Python. That includes time for development and testing.

For the complexity of the programs you'ld expect here, i.e., simple to mediocre, Python will -that's my opinion- in the hands of mediocre programmers give results faster by, oh, I think an order of two to four (which is not a big deal, we're not talking years here), assuming they know both languages. Some will just fail at writing anything coherent in Haskell (which is a big deal).

On the tools front, take a look at Visual Haskell. I haven't used it personally, but I would say that integration with VS is definitely a plus for those that prefer IDEs and the tools that come with them.

When it comes to designing programs in Haskell for which you'ld need an IDE, say 8 KLoc or more, you get to the point where you need exceptionally good programmers. I.e., intelligent, trained and using Haskell for more than half a year. At that stage, the only one who can possibly patch up an application with a visual interface faster than a trained person in Python/VB is probably Peyton-Jones.

[ I forgot to mention that even most academics from CS start out as programmers with poor skills. ]

[ Btw, this is not Haskell-bashing. I love it, it surely has its uses - especially where you want programs which do not fail, implement a spec to six sigma precision. But, yeah, my personal plain truth. ]

[ There will be a lot of angry COBOL programmers in the US staring dumbfounded at the Python shell. Don't expect a lot of good programmers at financial institutions, the field is too boring for them. ] [ The first point may actually be taken from a hidden agenda. ]

[ One of the real wins here might be that we now will have programmers doing normal requirements engineering, instead of just patching up programs which implement what they think a contract meant. ]

I have taught Haskell. I shifted from Clean because of its interactive interpreter. 80% of those programmers, which was on a Hogeschool/ Fachhochschule/ College / University-of-Professional-Education got it to the point that they could solve simple problems.

Thank you, and please continue to do so :). It seems that the programmers I know with a BS (or even Masters) in Computer Science feel uncomfortable outside of the OO world. Nothing against OO, but the one hammer for all problems can be pretty frustrating when encountered at work. Particularly when our definition and perceived benefits of OO differ (operational abstraction vs taxonomy).

Haskell, even with an interactive mode, is think-a-lot then do (think/ think/ think/ think/ do/ do).

I completely agree, this states succinctly what I was trying to get at with my "more time per LOC" paragraph. This is actually one of the things I love about Haskell, and a trait that I now carry over into other languages and tools. Interestingly, I find dynamic languages to be far more manageable when I take this approach, simply because there is less room for error.

You need academics of reasonable quality to program in Haskell, and those who can, should be in design/middle-management in industry. Not code-monkeys.

I am far from an academic. In fact I'm an autodidact. As a result I must beg to differ :). I'm not sure I agree that those that are the best programmers should be middle-management either... sounds like a way to waste a good brain. Not to mention it just sounds boring to me. If your assertion that only 3% of developers can effectively use Haskell holds, that would imply you have to design with the other 97% of developers in mind and your knowledge is wasted.

Different points, OO doesn't lead to spaghetti code. Python is an OO, but also a dynamic, language. OO is (mostly) fine, but known to fail at points. Dynamic languages allow for free-style hacking. Unless you constrain that, you'll end up with spaghetti code.

Fair enough, but I still maintain that OO (or functional) does not lead to good design. It can be a useful guide, but in the end it falls upon the programmers shoulders.

I think a claim: Once a proper Haskell program has been written (well) it holds little bugs, is valid. It's not only types, recursion and easily verified invariants play a role too.

I agree with this. After this explanation, I believe I took your original quote to mean more than what you actually did. I took "no reason to expect" as "no reason to test". Which you never actually said.

When it comes to designing programs in Haskell for which you'll need an IDE, say 8 KLoc or more, you get to the point where you need exceptionally good programmers. I.e., intelligent, trained and using Haskell for more than half a year. At that stage, the only one who can possibly patch up an application with a Visual Interface faster than a trained person in Python/VB is probably Peyton-Jones.

Good thing so many things that would take more than 8K LOC in say Java, takes a lot less in Haskell :)

This touches on something I have been thinking about for a while. Reading code written by others can be difficult in Haskell because it encourages an idiomatic style. On the other hand, I consider this to be one of the traits that gives Haskell it's power. Balancing the power vs readability can be rather difficult. This is not a new problem though, you could say Perl is even worse :) If there is a (language agnostic) document about the problem being solved and the technique formalized within it, the actual code is easier to grok. Unfortunately, it seems only academics have the time to do this on a regular basis.

It seems to me we are largely in agreement, I just have more faith in the average programmer. After all, they often build large, (mostly) working systems with very few (good) abstractions. While that is easier to learn, I would propose that it is more difficult in practice, particularly once the project is in maintenance mode. Maybe C# will slowly introduce the average programmer to non OO techniques and give them more reason to learn; not perfect, but a start.

[edit: small typo fix]

A few decades ago only scientists programmed. These days it's also reintegrating mothers, retrained sociologists, autodidact entrepreneurs, designers who started web-development, and whatnot. The pool of paid programmers must be at least a few hundred, maybe a few thousand, times as large as it used to be. Given the fact that Haskell is pretty unforgiving towards design errors, 3% might be an overestimation if you take into account that mediocre to large programs also need to be build.

Not everyone can program, you're an autodidact who can program in Haskell, which places you far out of the mean. You need to like it to be good at it, you need to like certain paradigms to become good at them, and even most CS students are, by-and-large, clueless about proper OO and FP when they leave the building, most are not even 'really good' at design. But that, they fix by having a lot of energy to throw at problems. ;)

[ On the good side. 3% of a substantial market is just good enough. ]

How so? Or more importantly, how does Python not give just as good of a formal specification? While any programming language does in some sense do this, and some may be closer than others, it doesn't make up for a real specification.

I would say it's because Haskell 98 actually has a specification, and Python does not. This gives real meaning to Haskell 98 expressions, though obviously not as much meaning as SML which has been fully formalized IIRC. But this is a good question: how much meaning does a specification convey vs. full formalization vs. just an implementation?

As a side point, one of the real wins here is that programmers now must do normal requirements engineering instead of patching up programs from what they think a contract, or a financial investor, meant. That makes the choice of the programming language somewhat irrelevant.

[Btw, on the formalization debate. It's just good enough for the time being. And you can't do it half. So, it's either fully formal, or not. And fully formal means defining a language, defining the meaning of values and operators (floating point decimal notation?), implementing it (by several companies?), and getting it into industry.

So. Formal spec, 1-3 years? Interpreters and software integration, 2 years? Adaptation and introduction into industry, 2 years? So, 5-7 years to get to a financial industry which will work with a standardized manner and fully defined contracts, possibly at the expense of small companies, and a good risk of failure anywhere in the process.

Standardizing on a Python (library) may just be the best choice. ]

I would say it's because Haskell 98 actually has a specification, and Python does not.

I'm clearly stretching here, but I can't resist. You could consider an implementation (CPython) of Python as it's specification... reductio ad absurdum.

But this is a good question: how much meaning does a specification convey vs. full formalization vs. just an implementation?

I agree this is a good question, full formalization vs just an implementation can be decided based on the existence of a proof of certain important properties of a code base, or at least it's core logic. In my opinion code bases without such a thing are simply implementations. This isn't necessarily a bad thing though.

I think the word specification is too ambiguous for an answer. A specification that I write if I plan on sharing with only other programmers is much different than a specification I give to a client.

A specification that I write if I plan on sharing with only other programmers is much different than a specification I give to a client.

The heart of the matter I guess.

In the pursuit of clarity, the SEC wants contracts, requirements documents, programs and data to avoid another expensive bail-out, maybe to see/analyze if there are other time bombs ticking, solve the current (and future) mess, and to have the best understanding of what these guys are doing.

They could have done worse.

I'm clearly stretching here, but I can't resist. You could consider an implementation (CPython) of Python as it's specification... reductio ad absurdum.

I figured you'd take the bait: the amount of semantic information in such a C specification is practically non-existent as compared to the semantic information in a Haskell or SML Python implementation. So I agree, an implementation is an executable specification, but the semantics of the language used for that specification dictates how much meaningful information it actually contains.

Pretty absurd?

I think there is at least one other disadvantage of an implementation as as a de-facto specification: it will prevent or at least impede development. It would become dangerous for the financial world to use a third party interpreter or analysis, because it might assume different semantics. While we, the potential writers of such tools, would be unable to conclusively show that our tools are conform to the implementation. Or that a certain 'feature' in the implementation is actually a bug.

So I would argue that it completely in our interest to standardise on a formal specification.

So I would argue that it completely in our interest to standardise on a formal specification.

As far as I can see, they put a leash on financial investors, and are investigating the mess. Though I agree that standardization probably will give a clear, more professional (faster) industry, I also wonder about its consequences.

Will it make it harder for small companies to start up/stay in business? Will it make more complex financial tools possible such that butterfly effects become near untraceable? To what extend can you formalize contracts? Will it make it harder for investors to sell contracts, i.e., will it speed up or slow down finance? And, what is in the interest of an economy and the public? [ Do financial institutions even want to give fully formalized contracts and data to the Sec? ]

The Sec/Us public/US economy/US bankers need this leash, it's in no-ones interest to have ticking time bombs under an economy. But, I am not sure the Sec even needs a full understanding of what is being sold (i.e., to the proverbial cent), more clarity of the contracts being sold and a leash may just be enough.

The trend is towards formalization, though. And I think that bankers themselves should push forward to standardization, just to make sure they are not doing it wrong themselves. (I.e., what do you do after a product/contract has been sold, the guy left, an no-one understands anymore what the guy was smoking when he sold it?)

[ Btw, does anyone have a feeling about the scale of this project? Is it even 'feasible?' How much data and programs can they expect? ]

[ Hehe, Ehud doesn't like me toying with hidden agendas. But it may well be that one reason is that bankers/Sec are not even interested in what mess is being dumped in their store, or formalization, but bankers/Sec just want a reason to have their whizz kids just write down what the hell they think they're doing, and just slow them down a bit. ]

A programming language doesn't have to include all possible features in its basic language defintion. This demand can lead to distorted language comparisons which don't even reflect common implementation practices. See my criticism of a comparison between TTCN-3 and Python which deals with a very different case but finally states the obvious.

in the limit, of course, this leads to the fear that the SEC intends the structure of the US financial system to depend on Guido von Rossum...

Managing the US financial system ( but why restrict the consideration to the US ) by a large, transparent community wasn't the worst idea ever.

But oh yes, the Freudian father complex: "Guido is my problem" and he denies me the human right for tail call elimination. That's why the world goes down and we shall take this incident with the humour it deserves. Haskell's messiah complex is much more creepy in comparison. But who wants it different? Humanity is dissent and drama.

I fully agree that having a formal semantics is not actually the primary concern. Yet that doesn't imply we should not have one. On the contrary, a formal semantics is a valuable tool.

The only argument against a formal semantics I can think of, is that it may slow down development of language extensions and the like (as argued in the History of Haskell paper by Peyton Jones et all), but in this case you wouldn't want the language to change too much anyway.

I'm not arguing against a formal semantics. I'm just surprised about what most here are focusing on as PL's offering to the problem: zeroing in on formal semantics, ironically, seems rather unprincipled ;-)

Edit: we don't define the semantics of a language on a whim; there's careful choice, such as when picking the form of the semantics. There are typically verification goals. Just having a semantics might not be enough for a desired goal (... and is more the norm than not). In the case of the SEC, I don't know what the goal is. Haskell or Scheme's semantics might not be much more useful than Python's reference implementation; the availability and practicality of simulation tools might be more important (which, oddly, points to Java or C).

Haskell or Scheme's semantics might not be much more useful than Python's reference implementation

Python's semantics can change significantly between releases. Why not stick with a semantics that is standardized and stable, like Haskell 98 or SML 97?

Why not stick with RISC? Haskell 98 and SML 97 may also be non-starters. If you're worried about the language changing, we can stick with a particular release of Python. I think you missed the point of my comment and clarification: before focusing on solutions (a language with a denotational semantics, operational semantics, reference implementation, ...?), focus on problem. I bet PLs have a lot more to offer than a precise notion of floating point.

What does exists is a body of people and institutions with respective agendas. At the same time, it's irrelevant to know the reasons towards no formalization, semi-formalization, or full formalization. It's just sufficient to tell them, that if they think one of those is a fit answer to the problem, what direction to take.

The solution as they propose is good enough for understanding financial products, but suboptimal if their goal is formalization.

Standardization on a moving target (Python), is impossible. At the same time, standardizing on a language for which value-safety isn't assured is also impossible for a financial industry. But also, Python is a great tool, and it's a justifiable choice to 'professionalize' an industry upon. I don't agree about your comment on simulation, except for performance issue, Python is a perfect tool for that, Java too, C only if you need real performance.

If their goal is formalization, then the answer is (academically) mostly easy. It is known how to standardize on a DSL. And, from an SE perspective, it is known how to go into such a process with clear goals, a risk analysis, a time frame, etc.

Academically, the perfect answer, you'ld expect a proposition to define a standardization committee to arrive at an open financial DSL (while they're using Python). Or, a light-weight solution, in case the SEC just wants some clarity, some Python distribution with a standard library for dealing with financial data and contracts.

Your post suggests the only thing languages have to offer is a standard with some mathematical and therefore precise (replicable) basis. If that's what you mean, and that's what LtU is about, then I'm on the wrong website.

Or, perhaps, their ultimate goal isn't formalization, and there are other things we can be offering?

[[Edit: more generally, formalization is really a means, not ends.]]

Your post suggests the only thing languages have to offer is a standard with some mathematical and therefore precise (replicable) basis. If that's what you mean, and that's what LtU is about, then I'm on the wrong website.

Did I say that? Nope, I was suggesting that depending on how much formalization, or precision, they need - academically,- a precise DSL would be the best answer if they need precision.

Or, perhaps, their ultimate goal isn't formalization, and there are other things we can be offering?

I have no idea what their goal is. I didn't read the proposal, just saw that they intend to use Python.

[ Actually, here we go again. What I first perceived as a leash, might as well be the opposite. Maybe it's just bankers' worry: Our IT departments, who lost half their pension, are not working well (anymore) with my financial gurus. Are we making enough money? And what is sold by ABS, another bomb? You never can tell. ]

It's just sufficient to tell them, that if they think one of those is a fit answer to the problem, what direction to take.

The solution as they propose is good enough for understanding financial products, but suboptimal if their goal is formalization.

I don't know what you mean by 'understand.' My computer runs x86 programs every day; I understand none of it.

The contract is there too. The Python tool is an extra to make precise and to see what different scenarios entail.

But granted, a suggestion to use part of UML for graphical description of decision flow might be sane too. Is that what you meant?

[ Got something wrong and edited the post ;) ]

That's an example but not really compelling.

The goal, as I understand it, is to allow investors to more easily calculate the value of a security so things like the wildly optimistic ratings given to CDOs by the rating agencies (contributing to the most recent crash) and Goldman Sach's current tussle with the SEC don't recur as frequently. This is usually done via Monte Carlo simulation so your first thought coincides with my current understanding. I think Python fails mightly for this task. It is too slow, it is too unstable, and it is too easily for a malicious developer to make the "waterfall programs" useless.

Concolic is a nice word I hadn't heard before.

Why are they doing this on ABS, and not on all financial products in general? It's not that ABS is that more difficult than a mortgage or other investment package.

[ Subsequently, in general, you cannot fix (bad) practice through software. Also, the purity of the goal depends on your amount of believe in free market economies. The US is polishing up and reinstating waterfall contracts by emphasizing on clarity. Maybe the pure and honorable course would be an outright ban on those, which is against US tradition. This is a US economy stimulation package, more (risky) loans for the public being secured, by measures which should provide more trust in waterfall deals, i.e., make it easier to sell them (again). ]

I guess it has more to do with the nature and number of variables involved. Mortgage contracts are actually very complex, spelling out many particular situations which could occur and their consequences. The securities are quite simple in comparison, as they have relatively few variables that have very well known quantifications.

For example, I very much doubt it would be possible to succinctly describe mortgage contracts at all. No matter the language used. While for example Peyton-Jones' paper on Financial contracts show that it is possible for e.g. options.

Then explain to me, why are they doing this on ABS, and not on all financial products in general?

Ummm... go ask the SEC dude. I don't make their decisions.

Let's just conclude they put the most measures where the perceived pain was the most. The proposal just solves a lot of problems, it doesn't actually regulate, or finish bad practice, it just introduces a lot more monitoring (also on deals which used to remain hidden). But it serves a lot of agendas.

[ Edited the post, the Sec proposal was also on derivatives, I thought, this just deals with ABS, securitization. ]

Depending on embedded DSL aka libraries used in Python, it doesn't have to be slow. I would assume the Python code only describes the mechanics of the contract, e.g.
if USD(1) < EUR(0.5) : cancelContract()
The simulations would be completely independent and could be programmed in a 'fast' language.

We know we are in trouble if they start including simulation software in the contracts themselves. Then who is responsible if reality doesn't match the simulation...

And one should have a moral obligation to be against programs which may lull a potential buyer into a false sense of security?

I.e., the running program doesn't give a good perspective on what an investor would be buying, and Python is too far of as descriptive language and a fully formal DSL is a better answer. (Though then the question again would become, what exactly is the benefit of a DSL over Python.) Would a potential buyer actually benefit from a formal description in a DSL? This actually might lead to one of the first cases where a court would order that programs should be written as unambiguous as possible, which would be a new thing in PL history.

[Sorry for shifting into the other direction, I cannot decide...]

[Maybe they'ld better stick a big warning/disclaimer on the program.]

[This is actually testing vs specification, but then for financial products.]

There are so many advantages to a DSL over a imperative simulation that it's hard to know where to start. With a DSL, contract descriptions could be stored in a repository. Contracts could be searched for in that repository in semantically interesting ways. Contracts could have analyses run on them that were unknown at the time of contract creation. Analyses and reports could be run over groups of contracts ("Show me our counterparty risk against Lehman for the Dec CDOs.") Repositories of contracts could be published to regulatory agencies, allowing systemic risks to actually be analyzed in real-time ("How bad off are we if Lehman goes down?").

Requiring an imperative implementation results in a bunch of useful one-off tools, at best. Requiring a declarative specification results in an ecosystem.

The proposal from the SEC can be read in two ways. A. We messed up, we're clearing to go back to business as usual, this is good for industry. B. We have a hard time these days securing (high-risk) loans, lets solve our problems with a new marketing tool.

A is good, laudable even. B, well, it's not in my interest to have European banks employ more gambling addicts because the US financial industry pushes marketing tools. Some loans just shouldn't be secured, some deals just shouldn't be made.

A DSL is the only good answer, and still may lead to the above result.

[ This may be a bit of an odd answer. But here, locally, in Europe, one bank went down in a deal which may only be described as "betting on a rigged horse." The excuse, financial products are hard, we don't understand what we were buying. Which is nonsense, they don't employ that many morons. Essentially, the problems were. A. loans were secured which could hardly be repayed (long term). B. Players were betting against each other on the outcome of payment. Clarity was never the issue. ]

I actually read this as a good argument against a single declarative language.

Requiring an imperative implementation results in a bunch of useful one-off tools, at best. Requiring a declarative specification results in an ecosystem.

Each of the operations you describe can be written as a "useful one-off tool" and can use some easy composition mechanism (like unix pipes). Why choose one language at all? Some of the functions will need to be formally verified, but other's will not. If the abstraction is at a process level instead of a language mechanism, the question of "what language?" becomes pointless (along with a host of other questions I bet).

Maybe instead of standardizing what language, what library, etc... It would be more productive to standardize on a file-format that can notate financial documents but does not specify an execution model; allowing the tools required to be made on demand in whatever fashion is appropriate.

What I was anticipating was a declarative specification language (no execution model implied), and I certainly didn't mean to imply that this should be an internal DSL written in any given language.

That said, the domain of financial instruments is rich enough that some languages will be more natural fits for these tools than others. In particular, a simple unidirectional composition mechanism like unix pipes is unlikely to be a good fit for the complex contingent networks of stocks and flows that portfolios of securities represent. Ideally, you would want a language in which it was convenient to express the various combinators that are used to compose financial contracts, and in which execution and transformation logics could be built over those combinators.

Ideally, you would want a language in which it was convenient to express the various combinators that are used to compose financial contracts, and in which execution and transformation logics could be built over those combinators.

I think we are talking about 2 different levels of abstraction. Processes + pipes should allow composition on a very high level and help tools integrate with each other. On the other hand, how these various tools are actually coded should be intentionally unspecified. Internally, using a combinator library similar to SPJ's would certainly be better, but orthogonal to composition at the process level.

I hope this doesn't stray too far into design/implementation for LtU.

Sounds dangerous, not only because a specific build has bugs, but also because the implementation will bit rot as OS APIs evolve.

Sure. It just seems better than the alternative which uses the name of a language, a name that does not refer to any single thing...

You almost sound like you want designation to mean something. And in the context of contracts, no less, which are an encapsulation of authority..

If you're not careful, you may find fingers slipping from that small, tenuously grasped ledge that is the home of semanticists, only to find that you have fallen into the full heresy of object-capabilities. :-) And we all know that will never come to anything. After all, Butler said so, so it must be true.:-)

Capabilities. I mean, dear God, Ehud. I'm truly concerned for you.