> Noise is anything that must be written for the program to function that is not relevant to the domain.

> ...

> What facilities does the language provide me to create correct-by-construction systems and how easily can I program the type-system.

Isn't programming the type-system orthogonal to the program's domain in the same way that manual memory management is?

No? I don't agree. The domain can be strongly modelled in the types; for instance, declaring kilometers, seconds, etc. instead of using primitive floats/reals everywhere, to statically prevent dimensional analysis issues.