They are not all that well typed. You can't have constrained types, for example (available with type classes in Haskell).

I spent long time with VHDL, which is Ada with third leg. It is not nice language to work with.

I also spend some time with stored procedure programming, mostly PL/SQL, most of them are also Ada based, and I find them quite productive, actually.

When you say constrained types do you mean generics? You have generics and concepts (similar to C++17) in Nim, not too sure about Ada.

I meant types with constraints, like this one: sum :: Num a => [a] -> a The type variable a is constrained to have implementation of interface Num (integer constant (0), addition, subtraction, etc).

These constraints can be much deeper. For example, I can define a function that allow me to add two somethings if their "regions" (a property I know how to compute) is equal and the result will be produced in "region" of first argument: add :: (Region a ~ Region b, Region a ~ Region c) => a -> b -> c

One use of something similar is addition of integer values represented by bit vectors in Verilog - you should not add bit vectors from different clock domains, otherwise you get unpredictable results.

Algebraic data types and ML-style modules are non-negotiable.

In Ada, you can get similar concepts via tagged records and generic packages.

Tagged records are one possible in-memory representation of sum values, perhaps the most sensible one. But I don't want in-memory representations of sum values. I want sum values themselves.

ML modules are much more than generic packages. ML's module system allows you to take an existing module, hide some of its components, make some of its concrete types abstract, and get a new module. My methodology of enforcing only one invariant in each module is impracticable without ML modules.