[Haskell-cafe] Knight Capital debacle and software correctness

[Jay Sulzberger]

On Sat, 4 Aug 2012, Clark Gaebel <cgaebel at uwaterloo.ca> 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 <jays at panix.com> wrote:
>
>>
>>
>> On Sat, 4 Aug 2012, Clark Gaebel <cgaebel at uwaterloo.ca> 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 <jays at panix.com> wrote:
>>>
>>>
>>>>
>>>> On Sat, 4 Aug 2012, Jake McArthur <jake.mcarthur at gmail.com> 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 <jays at panix.com> wrote:
>>>>>
>>>>>
>>>>>>
>>>>>> On Sat, 4 Aug 2012, Vasili I. Galchin <vigalchin at gmail.com> 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
>>>>>> Haskell-Cafe at haskell.org
>>>>>> 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
>>>> Haskell-Cafe at haskell.org
>>>> 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
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>
>>
>