I didn't see significant examples of Omega, but… I'd be surprised if a language with a Haskell-like syntax is verbose. The verbosity most likely didn't come f

I didn't see significant examples of Omega, but… I'd be surprised if a language with a Haskell-like syntax is verbose. The verbosity most likely didn't come from the language itself, but from the proofs. Once you've built the foundations, and proven a host of invariants about them, then you don't need to prove much more when you write the rest of the program. I bet Omega supports the very programming model you advocate: invulnerable foundations, and quickly written "rest of the program". If the code you saw was verbose, that's probably because it was foundation code. (After all, standard data structures are par of the foundations.)