I believe this (https://github.com/input-output-hk/plutus-prototype/blob/mas...) is the smart contract scripting language he's working on. Far from an expert on formal methods and language design, but, it does seem to be more fleshed out than the public information on Simplicity.