# Can you overload if-else-blocks? (for bounded model checking)

**URL:** <https://discourse.julialang.org/t/can-you-overload-if-else-blocks-for-bounded-model-checking/118364>\
**Category:** General Usage\
**Tags:** testing\
**Created:** [August 19, 2024, 9:04am UTC](https://discourse.julialang.org/t/can-you-overload-if-else-blocks-for-bounded-model-checking/118364 "2024-08-19T09:04:15Z")\
**Posts on this page:** 1\
**Showing post:** 3

<div class="post-metadata">

**Author:** ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)\
**Post date:** [August 19, 2024, 7:19pm UTC](https://discourse.julialang.org/t/can-you-overload-if-else-blocks-for-bounded-model-checking/118364/3 "2024-08-19T19:19:30Z")

</div>

Your intuition is pretty much on point from my POV, and you’ve also hit the same problem that people in the AD world encounter: branches mess up everything.

Basically, no, you can’t overload `if` from inside julia, since it’s not a function. See also [this previous discussion](https://discourse.julialang.org/t/how-bad-is-it-if-x-y-doesnt-return-a-bool/114611) about much the same topic.

That being said, you could theoretically build an interpreter of julia IR using the abstract interpretation framework, which ends up emitting not llvm IR, but SMT statements that you’d then feed to an existing solver like z3 or the like (or maybe some other solver, depending in what exactly you’re interested in).

Practically speaking though, this is still super difficult. The abstract interpreter interface is sparsely documented at best, and translating things like `x::Foo = ...` into an SMT clause is challenging, not to mention then actually proving useful properties. Specifications unfortunately [don’t compose](https://www.hillelwayne.com/post/spec-composition/) and even if they would do that cleanly, it’s still [super difficult](https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/) (if you only read one of these links, read this one) and complex to prove even [comparatively simple things](https://www.hillelwayne.com/post/nix/).

---

_[View the full topic](https://discourse.julialang.org/t/can-you-overload-if-else-blocks-for-bounded-model-checking/118364)._