Knight Capital debacle and software correctness

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
13 messages Options
Reply | Threaded
Open this post in threaded view
|

Knight Capital debacle and software correctness

Vasili I. Galchin
Hello Haskell Group,

    I work in mainstream software industry.

    I am going to make an assumption .... except for Jane Street
Capital all/most "Wall Street" software is written in an imperative
language.

    Assuming this why is Wall Street not awaken to the dangers. As I
write, Knight Capital may not survive the weekend.


Regards,

Vasili

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Ketil Malde-5
"Vasili I. Galchin" <[hidden email]> writes:

>     I am going to make an assumption .... except for Jane Street
> Capital all/most "Wall Street" software is written in an imperative
> language.

Tsuru Captial and Standard Chartered are also known to hire functional
programmers.

>     Assuming this why is Wall Street not awaken to the dangers.

As an explanation, this is a bit simplistic, I think. But I think the
reason these companies are willing to use experimental technology (as
Haskell is considered to be in industry), is that the consequences of
error can be so high.  For most mainstream software, users have been
trained to accept unreliability, and/or are not willing to pay the
costs.

Other examples of expensive software faults is the Ariane 5 launch and
the Sleipner A oil rig (that collapsed and sunk when in tow due to a mistake
in FEA strength calculations).

The space (and defense) industry have a long history of working towards
software security, but I think they have focused more on the software
process than on technology - ADA notwithstanding.  And probably rightly
so, even though technology can help you write correct code, there is
still plenty of rope.

-k
--
If I haven't seen further, it is by standing in the footprints of giants

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Jay Sulzberger
In reply to this post by Vasili I. Galchin


On Sat, 4 Aug 2012, Vasili I. Galchin <[hidden email]> wrote:

> Hello Haskell Group,
>
>    I work in mainstream software industry.
>
>    I am going to make an assumption .... except for Jane Street
> Capital all/most "Wall Street" software is written in an imperative
> language.
>
>    Assuming this why is Wall Street not awaken to the dangers. As I
> write, Knight Capital may not survive the weekend.
>
>
> Regards,
>
> Vasili

I believe this particular mild error was in part due to a failure
to grasp and apply category theory.  There are several systems here:

1. The design of the code.

2. The coding of the code.

3. The testing of the code.

4. The live running of the code.

5. The watcher systems which watch the live running.

If the newspaper reports are to be believed, the watcher systems,
all of them, failed.  Or there was not even one watcher system
observing/correcting/halting at the time of running.

Category theory suggests that all of these systems are worthy of
study, and that these systems have inter-relations, which are
just as worthy of study.

oo--JS.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Jake McArthur
I feel like this thread is kind of surreal. Knight Capital's mistake
was to use imperative programming styles? An entire industry is
suffering because they haven't universally applied category theory to
software engineering and live systems? Am I just a victim of a small
troll/joke?

- Jake

On Sat, Aug 4, 2012 at 12:46 PM, Jay Sulzberger <[hidden email]> wrote:

>
>
> On Sat, 4 Aug 2012, Vasili I. Galchin <[hidden email]> wrote:
>
>> Hello Haskell Group,
>>
>>    I work in mainstream software industry.
>>
>>    I am going to make an assumption .... except for Jane Street
>> Capital all/most "Wall Street" software is written in an imperative
>> language.
>>
>>    Assuming this why is Wall Street not awaken to the dangers. As I
>> write, Knight Capital may not survive the weekend.
>>
>>
>> Regards,
>>
>> Vasili
>
>
> I believe this particular mild error was in part due to a failure
> to grasp and apply category theory.  There are several systems here:
>
> 1. The design of the code.
>
> 2. The coding of the code.
>
> 3. The testing of the code.
>
> 4. The live running of the code.
>
> 5. The watcher systems which watch the live running.
>
> If the newspaper reports are to be believed, the watcher systems,
> all of them, failed.  Or there was not even one watcher system
> observing/correcting/halting at the time of running.
>
> Category theory suggests that all of these systems are worthy of
> study, and that these systems have inter-relations, which are
> just as worthy of study.
>
> oo--JS.
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Jay Sulzberger


On Sat, 4 Aug 2012, Jake McArthur <[hidden email]> wrote:

> I feel like this thread is kind of surreal. Knight Capital's mistake
> was to use imperative programming styles? An entire industry is
> suffering because they haven't universally applied category theory to
> software engineering and live systems? Am I just a victim of a small
> troll/joke?
>
> - Jake

ad application of category theory: No joke.

Atul Gawande's book The Checklist Manifesto deals with some of
this:

   http://us.macmillan.com/thechecklistmanifesto/AtulGawande

In related news, for every type t of Haskell is it the case that
something called "_|_" is an object of the type?

oo--JS.


>
> On Sat, Aug 4, 2012 at 12:46 PM, Jay Sulzberger <[hidden email]> wrote:
>>
>>
>> On Sat, 4 Aug 2012, Vasili I. Galchin <[hidden email]> wrote:
>>
>>> Hello Haskell Group,
>>>
>>>    I work in mainstream software industry.
>>>
>>>    I am going to make an assumption .... except for Jane Street
>>> Capital all/most "Wall Street" software is written in an imperative
>>> language.
>>>
>>>    Assuming this why is Wall Street not awaken to the dangers. As I
>>> write, Knight Capital may not survive the weekend.
>>>
>>>
>>> Regards,
>>>
>>> Vasili
>>
>>
>> I believe this particular mild error was in part due to a failure
>> to grasp and apply category theory.  There are several systems here:
>>
>> 1. The design of the code.
>>
>> 2. The coding of the code.
>>
>> 3. The testing of the code.
>>
>> 4. The live running of the code.
>>
>> 5. The watcher systems which watch the live running.
>>
>> If the newspaper reports are to be believed, the watcher systems,
>> all of them, failed.  Or there was not even one watcher system
>> observing/correcting/halting at the time of running.
>>
>> Category theory suggests that all of these systems are worthy of
>> study, and that these systems have inter-relations, which are
>> just as worthy of study.
>>
>> oo--JS.
>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Clark Gaebel-2
Yes.

On Sat, Aug 4, 2012 at 1:47 PM, Jay Sulzberger <[hidden email]> wrote:


On Sat, 4 Aug 2012, Jake McArthur <[hidden email]> wrote:

I feel like this thread is kind of surreal. Knight Capital's mistake
was to use imperative programming styles? An entire industry is
suffering because they haven't universally applied category theory to
software engineering and live systems? Am I just a victim of a small
troll/joke?

- Jake

ad application of category theory: No joke.

Atul Gawande's book The Checklist Manifesto deals with some of
this:

  http://us.macmillan.com/thechecklistmanifesto/AtulGawande

In related news, for every type t of Haskell is it the case that
something called "_|_" is an object of the type?

oo--JS.




On Sat, Aug 4, 2012 at 12:46 PM, Jay Sulzberger <[hidden email]> wrote:


On Sat, 4 Aug 2012, Vasili I. Galchin <[hidden email]> wrote:

Hello Haskell Group,

   I work in mainstream software industry.

   I am going to make an assumption .... except for Jane Street
Capital all/most "Wall Street" software is written in an imperative
language.

   Assuming this why is Wall Street not awaken to the dangers. As I
write, Knight Capital may not survive the weekend.


Regards,

Vasili


I believe this particular mild error was in part due to a failure
to grasp and apply category theory.  There are several systems here:

1. The design of the code.

2. The coding of the code.

3. The testing of the code.

4. The live running of the code.

5. The watcher systems which watch the live running.

If the newspaper reports are to be believed, the watcher systems,
all of them, failed.  Or there was not even one watcher system
observing/correcting/halting at the time of running.

Category theory suggests that all of these systems are worthy of
study, and that these systems have inter-relations, which are
just as worthy of study.

oo--JS.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Jay Sulzberger


On Sat, 4 Aug 2012, Clark Gaebel <[hidden email]> wrote:

> Yes.

Thank you!

Further, if you want:

   Let us have two types s and t.  Let _|_^s be the_|_ for type s,
   and let _|_^t be the _|_ for type t.

   For which famous equivalences of the Haskell System are these two
   _|_ objects equivalent?

oo--JS.


>
> On Sat, Aug 4, 2012 at 1:47 PM, Jay Sulzberger <[hidden email]> wrote:
>
>>
>>
>> On Sat, 4 Aug 2012, Jake McArthur <[hidden email]> wrote:
>>
>>  I feel like this thread is kind of surreal. Knight Capital's mistake
>>> was to use imperative programming styles? An entire industry is
>>> suffering because they haven't universally applied category theory to
>>> software engineering and live systems? Am I just a victim of a small
>>> troll/joke?
>>>
>>> - Jake
>>>
>>
>> ad application of category theory: No joke.
>>
>> Atul Gawande's book The Checklist Manifesto deals with some of
>> this:
>>
>>   http://us.macmillan.com/**thechecklistmanifesto/**AtulGawande<http://us.macmillan.com/thechecklistmanifesto/AtulGawande>
>>
>> In related news, for every type t of Haskell is it the case that
>> something called "_|_" is an object of the type?
>>
>> oo--JS.
>>
>>
>>
>>
>>> On Sat, Aug 4, 2012 at 12:46 PM, Jay Sulzberger <[hidden email]> wrote:
>>>
>>>>
>>>>
>>>> On Sat, 4 Aug 2012, Vasili I. Galchin <[hidden email]> wrote:
>>>>
>>>>  Hello Haskell Group,
>>>>>
>>>>>    I work in mainstream software industry.
>>>>>
>>>>>    I am going to make an assumption .... except for Jane Street
>>>>> Capital all/most "Wall Street" software is written in an imperative
>>>>> language.
>>>>>
>>>>>    Assuming this why is Wall Street not awaken to the dangers. As I
>>>>> write, Knight Capital may not survive the weekend.
>>>>>
>>>>>
>>>>> Regards,
>>>>>
>>>>> Vasili
>>>>>
>>>>
>>>>
>>>> I believe this particular mild error was in part due to a failure
>>>> to grasp and apply category theory.  There are several systems here:
>>>>
>>>> 1. The design of the code.
>>>>
>>>> 2. The coding of the code.
>>>>
>>>> 3. The testing of the code.
>>>>
>>>> 4. The live running of the code.
>>>>
>>>> 5. The watcher systems which watch the live running.
>>>>
>>>> If the newspaper reports are to be believed, the watcher systems,
>>>> all of them, failed.  Or there was not even one watcher system
>>>> observing/correcting/halting at the time of running.
>>>>
>>>> Category theory suggests that all of these systems are worthy of
>>>> study, and that these systems have inter-relations, which are
>>>> just as worthy of study.
>>>>
>>>> oo--JS.
>>>>
>>>>
>>>> ______________________________**_________________
>>>> Haskell-Cafe mailing list
>>>> [hidden email]
>>>> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>>>
>>>
>>>
>>>
>> ______________________________**_________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>
>>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Clark Gaebel-2
As far as I know, you can't check "equivalence" of _|_. Since Haskell uses _|_ to represent a nonterminating computation, this would be synonymous with solving the halting problem.

On Sat, Aug 4, 2012 at 2:04 PM, Jay Sulzberger <[hidden email]> wrote:


On Sat, 4 Aug 2012, Clark Gaebel <[hidden email]> wrote:

Yes.

Thank you!

Further, if you want:

  Let us have two types s and t.  Let _|_^s be the_|_ for type s,
  and let _|_^t be the _|_ for type t.

  For which famous equivalences of the Haskell System are these two
  _|_ objects equivalent?

oo--JS.



On Sat, Aug 4, 2012 at 1:47 PM, Jay Sulzberger <[hidden email]> wrote:



On Sat, 4 Aug 2012, Jake McArthur <[hidden email]> wrote:

 I feel like this thread is kind of surreal. Knight Capital's mistake
was to use imperative programming styles? An entire industry is
suffering because they haven't universally applied category theory to
software engineering and live systems? Am I just a victim of a small
troll/joke?

- Jake


ad application of category theory: No joke.

Atul Gawande's book The Checklist Manifesto deals with some of
this:

  http://us.macmillan.com/**thechecklistmanifesto/**AtulGawande<http://us.macmillan.com/thechecklistmanifesto/AtulGawande>


In related news, for every type t of Haskell is it the case that
something called "_|_" is an object of the type?

oo--JS.




On Sat, Aug 4, 2012 at 12:46 PM, Jay Sulzberger <[hidden email]> wrote:



On Sat, 4 Aug 2012, Vasili I. Galchin <[hidden email]> wrote:

 Hello Haskell Group,

   I work in mainstream software industry.

   I am going to make an assumption .... except for Jane Street
Capital all/most "Wall Street" software is written in an imperative
language.

   Assuming this why is Wall Street not awaken to the dangers. As I
write, Knight Capital may not survive the weekend.


Regards,

Vasili



I believe this particular mild error was in part due to a failure
to grasp and apply category theory.  There are several systems here:

1. The design of the code.

2. The coding of the code.

3. The testing of the code.

4. The live running of the code.

5. The watcher systems which watch the live running.

If the newspaper reports are to be believed, the watcher systems,
all of them, failed.  Or there was not even one watcher system
observing/correcting/halting at the time of running.

Category theory suggests that all of these systems are worthy of
study, and that these systems have inter-relations, which are
just as worthy of study.

oo--JS.


______________________________**_________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>




______________________________**_________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>




_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Jay Sulzberger


On Sat, 4 Aug 2012, Clark Gaebel <[hidden email]> wrote:

> As far as I know, you can't check "equivalence" of _|_. Since Haskell uses
> _|_ to represent a nonterminating computation, this would be
> synonymouswith solving the halting
> problem.

Ah, thanks.  I will attempt to think about this.

oo--JS.


>
> On Sat, Aug 4, 2012 at 2:04 PM, Jay Sulzberger <[hidden email]> wrote:
>
>>
>>
>> On Sat, 4 Aug 2012, Clark Gaebel <[hidden email]> wrote:
>>
>>  Yes.
>>>
>>
>> Thank you!
>>
>> Further, if you want:
>>
>>   Let us have two types s and t.  Let _|_^s be the_|_ for type s,
>>   and let _|_^t be the _|_ for type t.
>>
>>   For which famous equivalences of the Haskell System are these two
>>   _|_ objects equivalent?
>>
>> oo--JS.
>>
>>
>>
>>> On Sat, Aug 4, 2012 at 1:47 PM, Jay Sulzberger <[hidden email]> wrote:
>>>
>>>
>>>>
>>>> On Sat, 4 Aug 2012, Jake McArthur <[hidden email]> wrote:
>>>>
>>>>  I feel like this thread is kind of surreal. Knight Capital's mistake
>>>>
>>>>> was to use imperative programming styles? An entire industry is
>>>>> suffering because they haven't universally applied category theory to
>>>>> software engineering and live systems? Am I just a victim of a small
>>>>> troll/joke?
>>>>>
>>>>> - Jake
>>>>>
>>>>>
>>>> ad application of category theory: No joke.
>>>>
>>>> Atul Gawande's book The Checklist Manifesto deals with some of
>>>> this:
>>>>
>>>>   http://us.macmillan.com/****thechecklistmanifesto/****AtulGawande<http://us.macmillan.com/**thechecklistmanifesto/**AtulGawande>
>>>> <http://us.**macmillan.com/**thechecklistmanifesto/**AtulGawande<http://us.macmillan.com/thechecklistmanifesto/AtulGawande>
>>>>>
>>>>
>>>>
>>>> In related news, for every type t of Haskell is it the case that
>>>> something called "_|_" is an object of the type?
>>>>
>>>> oo--JS.
>>>>
>>>>
>>>>
>>>>
>>>>  On Sat, Aug 4, 2012 at 12:46 PM, Jay Sulzberger <[hidden email]> wrote:
>>>>>
>>>>>
>>>>>>
>>>>>> On Sat, 4 Aug 2012, Vasili I. Galchin <[hidden email]> wrote:
>>>>>>
>>>>>>  Hello Haskell Group,
>>>>>>
>>>>>>>
>>>>>>>    I work in mainstream software industry.
>>>>>>>
>>>>>>>    I am going to make an assumption .... except for Jane Street
>>>>>>> Capital all/most "Wall Street" software is written in an imperative
>>>>>>> language.
>>>>>>>
>>>>>>>    Assuming this why is Wall Street not awaken to the dangers. As I
>>>>>>> write, Knight Capital may not survive the weekend.
>>>>>>>
>>>>>>>
>>>>>>> Regards,
>>>>>>>
>>>>>>> Vasili
>>>>>>>
>>>>>>>
>>>>>>
>>>>>> I believe this particular mild error was in part due to a failure
>>>>>> to grasp and apply category theory.  There are several systems here:
>>>>>>
>>>>>> 1. The design of the code.
>>>>>>
>>>>>> 2. The coding of the code.
>>>>>>
>>>>>> 3. The testing of the code.
>>>>>>
>>>>>> 4. The live running of the code.
>>>>>>
>>>>>> 5. The watcher systems which watch the live running.
>>>>>>
>>>>>> If the newspaper reports are to be believed, the watcher systems,
>>>>>> all of them, failed.  Or there was not even one watcher system
>>>>>> observing/correcting/halting at the time of running.
>>>>>>
>>>>>> Category theory suggests that all of these systems are worthy of
>>>>>> study, and that these systems have inter-relations, which are
>>>>>> just as worthy of study.
>>>>>>
>>>>>> oo--JS.
>>>>>>
>>>>>>
>>>>>> ______________________________****_________________
>>>>>> Haskell-Cafe mailing list
>>>>>> [hidden email]
>>>>>> http://www.haskell.org/****mailman/listinfo/haskell-cafe<http://www.haskell.org/**mailman/listinfo/haskell-cafe>
>>>>>> <**http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>>  ______________________________****_________________
>>>> Haskell-Cafe mailing list
>>>> [hidden email]
>>>> http://www.haskell.org/****mailman/listinfo/haskell-cafe<http://www.haskell.org/**mailman/listinfo/haskell-cafe>
>>>> <**http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>>>>
>>>>
>>>>
>>>>
>>>
>> ______________________________**_________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>
>>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Steve Severance-2
In reply to this post by Ketil Malde-5
Actually Haskell is used in a surprising number of trading groups. However most people involved are contractually obligated to never talk about the technology in use at their firm. We make no secret that we use Haskell as our primary language in building trading systems. Other functional languages, notably F#, have seen significant uptake as well.

As to whether Haskell should/must/could be used an a particular system much of this choice (non-technology influences aside) is going to be bound by speed. As Knight is a market maker I would expect that the stock choice for rapidly evolving software is c++ on the intel compiler with a significant amount of strategies running on ASIC and FPGA. The reason being is that many strategies are relying on latency as a primary input to their success. 

We have the advantage of not being latency bound and we place a great amount of emphasis on correctness. We accept the fact that if we want to run latency bound strategies most of our runtime stack would be useless. If they had been using Haskell would they have still had whatever problem it was? At this point completely unknown. However the real world is a messy place and sometimes even haskell code has bugs.

Steve

On Sat, Aug 4, 2012 at 3:06 AM, Ketil Malde <[hidden email]> wrote:
"Vasili I. Galchin" <[hidden email]> writes:

>     I am going to make an assumption .... except for Jane Street
> Capital all/most "Wall Street" software is written in an imperative
> language.

Tsuru Captial and Standard Chartered are also known to hire functional
programmers.

>     Assuming this why is Wall Street not awaken to the dangers.

As an explanation, this is a bit simplistic, I think. But I think the
reason these companies are willing to use experimental technology (as
Haskell is considered to be in industry), is that the consequences of
error can be so high.  For most mainstream software, users have been
trained to accept unreliability, and/or are not willing to pay the
costs.

Other examples of expensive software faults is the Ariane 5 launch and
the Sleipner A oil rig (that collapsed and sunk when in tow due to a mistake
in FEA strength calculations).

The space (and defense) industry have a long history of working towards
software security, but I think they have focused more on the software
process than on technology - ADA notwithstanding.  And probably rightly
so, even though technology can help you write correct code, there is
still plenty of rope.

-k
--
If I haven't seen further, it is by standing in the footprints of giants

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Florian Weimer
In reply to this post by Vasili I. Galchin
* Vasili I. Galchin:

>     I am going to make an assumption .... except for Jane Street
> Capital all/most "Wall Street" software is written in an imperative
> language.

I expect that most of it is written in Excel, which doesn't really
qualify as an imperative language.  High-frequency trading is likely
different, but that covers just a fraction of the software being used
for trading.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

Jon Fairbairn
In reply to this post by Jay Sulzberger
Jay Sulzberger <[hidden email]> writes:

> On Sat, 4 Aug 2012, Clark Gaebel <[hidden email]> wrote:
>
>> As far as I know, you can't check "equivalence" of _|_. Since Haskell uses
>> _|_ to represent a nonterminating computation, this would be
>> synonymouswith solving the halting
>> problem.
>
> Ah, thanks.  I will attempt to think about this.

Also, one way of looking at type systems says that all these
_|_s are the same (but as Clark says, there’s no way within
Haskell to compare them). Haskell mangles this a little by
including non-value things other than non-termination in its
types.

   — Jón


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Knight Capital debacle and software correctness

scooter.phd@gmail.com
In reply to this post by Steve Severance-2
From some of the reports in the press, the problem was that the trades were supposed to be spread out over several days or weeks, but were spread over hours instead. So, if that were true, no type system would be of any help.

The US Navy had a similar problem on a propulsion control system back in 1995/96, where all consoles went into blue screens of death and the cruiser in question had to be towed back to port from ~15 nautical miles off shore. In the root cause analysis, it turned out that a particular form field should never have been allowed to take on the value zero, which ended up causing a NT kernel crash in a control system driver. Moreover, the bad value was replicated across all control system machines, thereby crashing the entire control system.

Job number one in a US Navy engineering department: keep the props rotating. If the ship has propulsion, it can do things, like get out of the way of danger.

Faults occur for a variety of reasons.


-scooter

On Sat, Aug 4, 2012 at 12:14 PM, Steve Severance <[hidden email]> wrote:
Actually Haskell is used in a surprising number of trading groups. However most people involved are contractually obligated to never talk about the technology in use at their firm. We make no secret that we use Haskell as our primary language in building trading systems. Other functional languages, notably F#, have seen significant uptake as well.

As to whether Haskell should/must/could be used an a particular system much of this choice (non-technology influences aside) is going to be bound by speed. As Knight is a market maker I would expect that the stock choice for rapidly evolving software is c++ on the intel compiler with a significant amount of strategies running on ASIC and FPGA. The reason being is that many strategies are relying on latency as a primary input to their success. 

We have the advantage of not being latency bound and we place a great amount of emphasis on correctness. We accept the fact that if we want to run latency bound strategies most of our runtime stack would be useless. If they had been using Haskell would they have still had whatever problem it was? At this point completely unknown. However the real world is a messy place and sometimes even haskell code has bugs.

Steve


On Sat, Aug 4, 2012 at 3:06 AM, Ketil Malde <[hidden email]> wrote:
"Vasili I. Galchin" <[hidden email]> writes:

>     I am going to make an assumption .... except for Jane Street
> Capital all/most "Wall Street" software is written in an imperative
> language.

Tsuru Captial and Standard Chartered are also known to hire functional
programmers.

>     Assuming this why is Wall Street not awaken to the dangers.

As an explanation, this is a bit simplistic, I think. But I think the
reason these companies are willing to use experimental technology (as
Haskell is considered to be in industry), is that the consequences of
error can be so high.  For most mainstream software, users have been
trained to accept unreliability, and/or are not willing to pay the
costs.

Other examples of expensive software faults is the Ariane 5 launch and
the Sleipner A oil rig (that collapsed and sunk when in tow due to a mistake
in FEA strength calculations).

The space (and defense) industry have a long history of working towards
software security, but I think they have focused more on the software
process than on technology - ADA notwithstanding.  And probably rightly
so, even though technology can help you write correct code, there is
still plenty of rope.

-k
--
If I haven't seen further, it is by standing in the footprints of giants

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe