I was short on time, so only submitted a couple of reference implementations, not actual FunC programs (not pretending on any kind of prize). One of them is in TypeScript which describes the multi-siganture wallet. As all imperative languages are pretty much the same, it can be translated to FunC straightforwardly. Another is in Idris (functional language with dependent types), and it explores the possibilities of static (compile-time) guarantees, that smart contract behaves precisely under the given specification.