[unboxed_type]

It is hard to imagine that a proof-assistant will be used as a tool for checking smart-contract correctness due to a lack of sufficiently trained personal. What this BC community is really need is a suitable programming language which will be tailored for functional correctness and expressiveness. Unfortunately, the Simplicity language addresses only the first half, and it is not sufficient for practical success IMO.