Re: How to get Ada to “cross the chasm”?

[Paul Rubin <no.email@nospam.invalid>]

"Dan'l Miller" <optikos@verizon.net> writes:
> then some of those incoming transactions are going “fall on the
> cutting room floor” so to speak—the proverbial bit bucket.

That's not how those transactions.  They're not datagrams and they don't
fall on the floor.  If they don't get through there is a retry.  

>> Their machines are not in data centers.
> The heck they are not!  Arbitrage traders place their servers as close
> to telecom data centers (called central offices) as they can get!

I've always heard that low latency HFT traders want to put their gear in
the same building as the financial exchange, maybe even right on the
trading floor or next to it.  They wouldn't want to be miles away in a
data center.  I'll ask about this though.  I'll admit that I thought of
"data center" as meaning "internet" rather than direct fiber, and that
wasn't exactly right.

> Second in the race misses the deadline, and is considered total
> failure, because the arbitrage opportunity was lost (along with
> hundreds of thousands or millions of dollars).

That sounds like nothing was lost, but rather, a potential gain wasn't
realized.  Those guys do 1000s of transactions a second and don't care
if they miss a few.  They've got a box that steadily converts
electricity to money, like bitcoin mining.  If they turn it off for a
few minutes, the money stops during the downtime, but nothing bad
happens.  They don't LOSE money while it is off.

Also, they want the opposite of critical systems development.  Thought
experiment: you proudly deliver your SPARK-verified Ada HFT system to
your Wall Street customer.  They turn it on and it generates profits and
they are happy.  Now some demented C programmer comes along and wants to
swap out your beautifully verified inner loop with some crazy pointer
mangling and type casting madness.  This not only invalidates your SPARK
proofs, but it's actually explicitly undefined behaviour according to
the C standard.  But 1) it empirically seems to work, at least on some
particular combination of compiler, version, and optimization flags; and
2) it runs 1% faster than your Ada code.

What do you think happens next?  My bet is they want the speedup and
don't care about the proofs.