Can someone explain to me why they chose to make their own language instead of creating a DSL inside of an existing language?
Daily LoL: Googling "secure language" brings up mostly results about Java.
https://publications.lib.chalmers.se/records/fulltext/234939...
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.
Starting from something like the lambda-calculus seems more sensible than starting from something like Javascript.
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.
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.