Matrix programs are taking increasing important role in the intelligent systems. As the complexity of matrix applications grows, the difficulty of producing correct matrix code does the same. Parallel hardware can greatly increase the speed of matrix operations; nevertheless, using parallel hardware for programming to achieve parallel operations requires programmers to describe functions in the program and to manage how to use hardware resources to deliver results. These programs are usually written in imperative languages that are difficult to reason about and refactor for different parallelization strategies. A matrix expression code generation technology has been implemented from high-level matrix operators to C code in Coq, which can convert functional matrix code with execution strategies into efficient low-level imperative code. In the future, the formal verification of the matrix will be integrated with the automatic generation of matrix code, and formal verification of the matrix code conversion process will be performed to ensure the reliability of the generated matrix code, laying the foundationfor the development of a high-reliability deep learning compiler based on the matrix formal method.