[Haskell-cafe] Knight Capital debacle and software correctness

[Clark Gaebel]

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.

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>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120804/57201e87/attachment.htm>