Enlightening article trying to verify leftpad (+2 other small functions) in a range of theorem provers: https://www.hillelwayne.com/post/theorem-prover-showdown/
miniblog.
Related Posts
Solving Fizzbuzz using Euler's totient theorem rather than conditionals:
Solving Fizzbuzz using Euler's totient theorem rather than conditionals: https://philcrissman.net/posts/eulers-fizzbuzz/
Untyped programs don't exist: https://www.williamjbowman.com/blog/2018/01/19/untyped-programs-don-t-exist/
Demonstrates a simple theorem, but has a nuanced notion of types as invariants. It discusses the important questions of when we should check types, allowing escape hatches, and whether type checking should be decidable.