I haven’t managed to make much progress on it since. There was some nice research done J. Urban (and also by Facebook Research) in this direction but I’m not aware of anything else. Indeed Coq seems hard at the beginning and there might be other languages which would be better to work with on machine learning level. My idea, not fully developed, was to try to build a new language — think TeX with implemented basic logic — which would be purely suited from start for ML. I got however defeated by technical difficulties back then, and other projects became more important. Though if you have anything interesting to share on this subject, I’m happy to learn more!