Missing automated tests for "How to use Dafny to prove type safety"

[alex-chew]

The make check target is used for automated verification of Dafny code in blog posts (both in CI and locally) in order to avoid stale code in blog posts. This requires the Dafny code to be manually extracted from posts' Markdown files (in _posts) and for the verification commands to be added to the Makefile (typically by running a script alongside the extracted Dafny code).

The "How to use Dafny to prove type safety" post is not currently being verified automatically because the above requirements are not met.