# Julia with respect to reliability, sustainability, critical application, dynamic/static typing, big data, HPC?

**URL:** <https://discourse.julialang.org/t/julia-with-respect-to-reliability-sustainability-critical-application-dynamic-static-typing-big-data-hpc/23135>\
**Category:** Performance\
**Created:** [April 14, 2019, 11:44am UTC](https://discourse.julialang.org/t/julia-with-respect-to-reliability-sustainability-critical-application-dynamic-static-typing-big-data-hpc/23135 "2019-04-14T11:44:03Z")\
**Posts on this page:** 1\
**Showing post:** 21

<div class="post-metadata">

**Author:** ![chakravala](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/chakravala/32/6832_2.png) [@chakravala](https://discourse.julialang.org/u/chakravala)\
**Post date:** [April 16, 2019, 2:00pm UTC](https://discourse.julialang.org/t/julia-with-respect-to-reliability-sustainability-critical-application-dynamic-static-typing-big-data-hpc/23135/21 "2019-04-16T14:00:51Z")

</div>

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](http://hal.inria.fr/docs/00/98/76/10/PDF/ReflectionProofs.pdf)

> 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?

---

_[View the full topic](https://discourse.julialang.org/t/julia-with-respect-to-reliability-sustainability-critical-application-dynamic-static-typing-big-data-hpc/23135)._