Yes, but usually the thing that comes out of this process is having less rich types and separating proofs from computation. (Example: working with length-indexed lists in https://github.com/mit-plv/fiat-crypto was a lot more painful for writing cryptographic algorithms than using plain lists and proving length-preservation separately with tactics. Probably because the length is not an inherent part of the algorithm.)