Function Contracts Blogpost (#44)

Adds a new blog post about the function contracts feature including a walk-through of an example from Firecracker.

Includes description modular verification, inductive verification and sketches how contracts work internally.

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
Co-authored-by: Patrick Roy <roypat@amazon.com>