27 ms·
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.
by snaky 8y ago
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.
- twic 8y agoIs it possible to synthesize hardware from Coq?
- mruts 8y agoNot 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/ https://www.janestreet.com/tech-talks/ocaml-all-the-way-down...
- snaky 8y agoYes. https://deepspec.org/entry/Project/Kami https://deepspec.org/entry/Project/Kami http://conal.net/blog/posts/haskell-to-hardware-via-cccs http://conal.net/blog/posts/haskell-to-hardware-via-cccs