I haven't used it, yet, though I want to, so I don't know how much of the following applies to Catala specifically, yet.
I worry that "correct by construction" encodings actually make it harder to encode existing legislation with errors, and then use testing and analysis to demonstrate the existence of the error. If you are forced to rely only on compiler errors, you lose access to information. Strict languages may also force you to make certain assertions that are not included in the law, and may not be legally true. I haven't yet done any encodings in strict languages, but Catala will likely be the first one I try.
Isomorphism between the law and the encoding is critically important to ease of use and maintainability for legal knowledge engineers. Because of how law uses defeasibility, you can't get isomorphism without default logic (or another non-monotonic alternative). But default logic is not also not enough on its own. You need syntax that eliminates the need to name the justifications inside the code for the default. Because in real laws, the information about what justifications apply to a default is sometimes included in the segment of the legislation that expresses the default ("default a is true, subject to section 2"), and sometimes it is included in the segment of the legislation that expresses the exception ("notwithstanding section 1, exception b is true").
There lots of other nice-to-have features for getting defeasibility and isomorphism at the same time, but the upshot is that for that purpose default logic is necessary and insufficient.
As far as demerits are concerned, checking for the presence of exceptions, particularly when they are implied to potentially exist, is going to be slower; it has multiple semantics, so you have to pick one or let the user pick one; and the more isomorphic the code, the less clear the semantics become, which makes some things implict in the encoding that are neither implicit nor explicit in the legislation.
Jason