Transactional vs. provable semantics A lot of package systems out there do transactional semantics. try to update if it f* up, go back to previous state. We do provable replacements compute as much as we can to ensure things won't fail once we're satisfied, do the replacement (that can't fail) Works most of the time We now have tools (pkg_check, 2010) in the remaining cases.