Interesting that you mention this. I know when I am writing C, I usually "malloc" dynamic data structures, whereas in Haskell, I usually "alloca" dynamic data structures (when talking to C libraries, obviously). Same end result, but alloca is actually faster, which makes allocation-heavy libraries faster when used from Haskell. (I guess I should use alloca in C, too. But I've never seen this anywhere.)

I noticed that this was especially helpful in a library I recently used that never allocated any of its own memory; it was always the responsibility of the caller. Haskell idioms worked much better than C idioms here.

I'm a bit confused about why you think operating within a monad causes problems for proving correctness; to my knowledge, verifying code which uses monads is no more difficult than code using any other data types.

Wait, are you saying that calling a function called "(>>=)" is no different than calling any other function? Shocking. :)