transferAmount(from: Account, to: Account, amount: Money)

How can a type system know that you are passing the accounts in the correct order?

You might start by trying to make more strict types such as SourceAccount and DestinationAccount.

  transferAmount(from: SourceAccount, to: DestinationAccount, amount: Money)

But we know that any account is likely to be both of these at different times. We only persist Accounts and have to convert at runtime. Now you face the challenge of converting a regular Account to a FromAccount.

  src := fromAccount.toSourceAccount()
  dest := toAccount.toDestinationAccount()
  transferAmount(src, dest, amt)

How can the type system know that you are converting the correct Account? The type system cannot determine what is semantically correct. It's a recursive problem.

What you are saying is all correct, but I think we disagree about the terminology. You said "the type system can never know what is semantically correct" but I think the right way of saying it is "the type system can sometimes not know what is semantically correct".

Because in practice, code like "src := fromAccount.toSourceAccount()" is very rare and happens at system boundaries or logic boundaries once - after that, all semantical errors can be caught by the typesystem, and this accounts for the vast majority of the code.

So yes, the typesystem can and will prevent semantical errors. But it can not protect you from making them in all cases, that's impossible.

A programmer will still need to write correct code, but in your first example the error happens at the boundary between two modules. In the second example, the error is fully contained within one module.

One of those two is easier to spot, either by the original programmer, or by a code reviewer, or by someone trying to track down a fault.

If all the type system does is make semantic errors easier to spot and fix, it's still offering a lot of value.