Fantastic blog post demonstrating how to write your own clang analysis: https://ehsanakhgari.org/blog/2015-12-07/c-static-analysis-using-clang#comment-3494 (compilers are great for nonlocal reasoning)
miniblog.
Related Posts
I'm a huge fan of languages that require you to explicitly export your functions (e.g. pub in Rust or export in JS).
It's much easier to change than a separate header file (.h in C, .mli in OCaml) and it enables local reasoning. You can see from the definition if it's exported.
Great, thoughtful discussion about the direction Racket wants go in. The reasoning is given and broader language goals are shared, way beyond syntax.
A metacircular interpreter in Prolog: https://www.metalevel.at/acomip/
The fact that this exists at all is mindbending to me. It's easy to just see Prolog as a logical reasoning engine.