Agda is a logical programming language and theorem prover, that have bring my attention for being compiled by default and by providing support for Category Theory, which allows it to be used at some very elementary level, and being comparable to some theorem provers such as Coq.
The case I am considering is when the existence or non existence of certain properties, which could be proved, would determine the necessity or not of including some code or how that code should be written, for the achievement of the program goals, or to guarantee its consistency with the rest of the program, or internal – such as, could we provide facts for bringing rules for changing code, for avoiding unexpected errors? or return to some problematic execution with different code, if checking would be done later?
It is something that could be useful for objectives whose executions are much dependent on the context of data; such as optimizations or robots
Also the ability to use evaluation in Julia is something that maybe could make it further usefull