HOL is written in OCaml. The likely answer is because integrating OCaml and TensorFlow would be painful -- and OCaml isn't one of the languages Google supports internally [1]. Probably was easier to reimplement than to try to do all the contortions needed to use it in this context.
(I work part time on the Brain team, but I haven't asked the authors about this -- this is a best guess based upon knowing TF, not an informed statement.)
(I work part time on the Brain team, but I haven't asked the authors about this -- this is a best guess based upon knowing TF, not an informed statement.)
[1] https://www.quora.com/Which-programming-languages-does-Googl...