[triska]

Thank you a lot for taking the time to respond!

Could you please give a short example of how we can use Catala to interpret for instance the sample program that is shown on the project page? Does it have a natural representation as a Catala data structure that can be reasoned about conveniently within Catala?

[denismerigoux]

No, the language does not have self reflection, it is a domain specific language that is not even Turing complete. However Catala programs could be compiled to deep or shallow embeddings inside other programming languages, including inside theorem provers interactive (Coq, F*, Agda, etc.) or automatic (SMT solvers, abstract interpreters). You would then be able to reason about your Catala programs inside these external provers.