Syntax aside, are verified smart contracts a solution looking for a problem?
They were supposed to be the killer app for blockchain-based solution, but they are computationally (and architecture-wise) prohibitively expensive, slow and just too complicated given the problems they can and can't solve. Am I wrong here? You can always cheat a 'smart' contract outside of blockchain?
> Scilla is not meant to be a high-level programming language, and we are going to use it as a translation target for high-level languages, such as Solidity, for performing program analysis and verification, before further compilation to an executable bytecode.
Based on that extract from the abstract, I would say human readability and writeability are not the main goals of the language. Still, the syntax doesn't look impenetrable to me. Is there anything in particular about this excerpt you find hard to read? The whitespace is better in the original.
(* Transition 2: Sending the funds to the owner *)
transition GetFunds
(sender : address, value : uint, tag : string)
(* Only the owner can get the money back *)
if (tag == "getfunds") && (sender == owner) ⇒
blk ← && block_number;
bal ← & balance;
if max_block < blk
then if goal ≤ bal
then funded := true;
send (<to → owner, amount → bal,
tag → "main", msg → "funded">, MT)
else send (<to → owner, amount → 0,
tag → "main", msg → "failed">, MT)
else send (<to → owner, amount → 0, tag → "main",
msg → "too_early_to_claim_funds">, MT)
