Here's a master's thesis by a couple guys who made Idris compile to Ethereum bytecode.

https://publications.lib.chalmers.se/records/fulltext/234939...

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.

You might be interested in W7, an object-capability Scheme variant: http://mumble.net/~jar/pubs/secureos/secureos.html

Starting from something like the lambda-calculus seems more sensible than starting from something like Javascript.

> What language would you choose?

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.

Ada.