Abstract: This paper proposes an automatic programming system based on Martin-l(?)f's TypeTheory Algebraic specifications about problems are taken as depth knowledge in the system and thedepth knowledgebase of the system is constructed.For a specification of a problem proposed by theuser to the system.the system gives a program satisfying the specification as an answer.The systemrealizes initially the integration of the specification.construction and verification in software formaldevelopment.