PrimeNumber is definitely possible in pretty much any dependent type language. Indeed, it would be pretty impossible to get any work done in Lean without it.

TotalProgram: possible in some, not in others, I think.

> PrimeNumber is definitely possible in pretty much any dependent type language.

That's awesome! Thank you. I didn't know type systems were capable of expressing that level of sophistication.

Would HaltingProgram and NonHaltingProgram be expressible? I hope it's clear what I'm trying to convey, but the technical wording escapes me today.

HaltingProgram and MaybeHalting is expressible(or vice versa), if you want to cover all programs in one of two types. If you want specifically HaltingProgram and NotHaltingProgram then you need a third category of MayOrMayNotHaltingProgram.

There is a fascinating result about types that they have a one to one correspondence with proofs. Dependent type systems leverage that to the hilt.

see the 'total' keyword in Idris

https://docs.idris-lang.org/en/latest/proofs/patterns.html