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.

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.

Naivety, youth.

Too young, too simple, sometimes naive.

Now who the hell gave them any money for that?

Investors who have FOMO (fear of missing out).

+No Clue.

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.

Hubris.

This new language for Ethereum by Vitalik is exactly what you said: https://github.com/ethereum/viper

Viper's inspired by Python, which (for all the nice things we can say about it) is a _terrible_ place to go for inspiration for this kind of task.

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.

It's about costing the operations reliably.

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.

In the rationale document they explain that arbitrary length integers were too difficult to determine a reasonable gas cost around for math etc.

"Normal" and "secure" languages don't do this already?