What language would you choose? AFAIK there are almost no _actually_ secure languages. The ones that exist (e.g. Idris, Agda) are notoriously hard to use (although their Turing "incompleteness" is arguably a feature for smart contracts/distributed computations).
Daily LoL: Googling "secure language" brings up mostly results about Java.
Idris isn't difficult to use for things that don't require tons of library support (since there aren't many libraries to speak of yet), unlike Agda, which is far from a programming language in the usual sense (it's a proof assistant, and you're only really supposed to typecheck stuff with it).
You can just skip messing with the termination checker (just don't mark your functions total) in Idris and write Haskell-ish code. The occasional rough edge aside, it's not hard to write the kind of programs we're talking about here: and if you want to prevent DDoS-like infinite looping, put the "total" annotations back in.
The E language has been a vehicle for smart contract research for decades. Joe-E is a more recent incarnation of many of the same ideas, that's a secure subset of Java.
When I took a look at it, two or three years ago, I think there were three different guys in the organization each busy with his own idea of a high-level language to put on top of the VM, each inspired by a different GP language. That signaled a certain lack of focus.
Viper is only inspired by Python's syntax. It's not a highly reflective completely dynamic language like Python. (But this also means that it is not a "DSL inside of an existing language", contrary to what your parent claimed.)
This is because running code on Ethereum VM and storing data is hugely expensive (rightly so, as it's being done on all nodes in the world). Therefore Solidity will try to compile into a VM code that uses the least numbers of cheapest instructions and pack data into as small memory package as possible.
Most of the issues pointed out by int_19h would be handled at compile time during static analysis and wouldn't change much to the generated bytecode. I'm talking about strong typing, immutability by default, less error-prone syntax, tail calls, evaluation order etc...
Even replacing 256bit ints with arbitrary precision "bigints" wouldn't add too much of a cost if it's a native type of the underlying VM (as it should be for such an application IMO). It might even reduce code size by removing overflow tests.
But I would still expect arithmetic to be overflow-checked by default, as in e.g. VB.NET. This would mean that careless arithmetic on unvalidated inputs could still cause the contract to fail - but at least it would be a controllable failure, with all state changes being reversed, and hence not exploitable.
