Unlikely any time soon - most HFTs will have massive, battle-tested C++ code bases already. The data ownership model in HFT is usually very clear - receive packet, pass through some processing pipeline, emit packet, on the same thread. If you want to send data into another part of the system (eg. because different threads handle different securities), posting a message onto their event queue works well.

Not happening.

Rewriting some hot path parts of the stack in Verilog is a usual thing, and rewriting some other parts in Coq is the future.

Is it possible to synthesize hardware from Coq?

Not entirely on topic, but Jane Street (HFT ETF market maker) wrote an OCaml to FPGA compiler

https://www.janestreet.com/tech-talks/ocaml-all-the-way-down...

Yes.

https://deepspec.org/entry/Project/Kami http://conal.net/blog/posts/haskell-to-hardware-via-cccs

The threading feature that are not stable / experimental? There is not way someone is moving to Rust for this.