This might interest you if you like the idea of proving properties of programs.

https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_corresp...

It's actually not a lot of work and very rewarding to write a proof-checker that uses this principle.