I can see many problems can be solved with modern symbolic approaches like theorem provers, dependent types, pattern matching etc. But I will have to dive in to actually confirm it.