[nequo]

I do wonder if a dependently typed language like Agda or Idris would be a better choice for something like sudo. They are not terribly slow (to run), by today they are well-understood, and they can formally prove invariants about the program.

[pdimitar]

Could be. Having both strong static typing (and a more formal one) and less code will help a lot.