A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code