Not really, as you always need to check back on your assertions, especially at the boundary points where information about types and ownership are more axiomatic than the result of logical inference.
Sure, but there are less assertions to check. The surface area and boundaries are smaller and more limited.