Visible to the public Analysis-Based Verification: A Programmer-Oriented Approach to the Assurance of Mechanical Program Properties