> 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?