Having type-safe/correct software is a huge benefit when you're controlling machinery
program vehicle computers that control hybrid
powertrains for heavy duty trucks -- garbage to be
specific. Our systems interface with engines,
transmissions, brake controllers, and yes, accelerator pedals.
Haskell GADTs ensure type correctness of the generated
C code. I find it interesting that a type system in
one language can prevent type problems in another.