The Ethereum VM accepts opcodes like any other modern computing platform. There's a lot of work going into formal verification of contract code. There's nothing in principle that prevents compilation of smart contracts into VM code via a formally verified compiler that implements a functional language.
I'm an Ethereum smart contract dev/auditor and active in the community. I'm not aware of any ideological opposition to more functional or verifiable languages.
In fact, there are several new languages in development to move things in that direction, including Vyper (originally designed by Vitalik) and Bamboo (designed by the person employed by the EF to work on formal verification).
My experience proposing actual use of these has been met with complaint and actual jeers in social circles. Further, it's pretty depressing that you suggest Vyper and Bamboo actually offer more formal verification or even correctness.
I don't see either trying to adopt approaches more like Simplicity.
