[OneWingedShark]

Honestly, Ada fits a LOT of that bill.

The type-system and forced spec/implementation split both work well to catch errors; you can go further with SPARK [proving] and using Pre- and Post-conditions, type-invariants.