The only reason I mention it is purely due to my interest in the mathematics of it, I recommend looking at the referenced paper Engineering Proof by Reflection in Agda
Abstract. This paper explores the recent addition to Agda enabling reflection, in the style of Lisp and Template Haskell. It gives a brief introduction to using reflection, and details the complexities encountered when automating certain proofs with proof by reflection. It presents a library that can be used for automatically quoting a class of concrete Agda terms to a non-dependent, user-defined inductive data type, alleviating some of the burden a programmer faces when using reflection in a practical setting.
what does @jeff.bezanson have to say about it with respect to Julia?