ในวิทยาการคอมพิวเตอร์การสร้างโปรแกรมขึ้นมาใหม่หมายถึง การสร้างโปรแกรมจากข้อกำหนดของโปรแกรมนั้น โดยใช้วิธีการทางคณิตศาสตร์

การสร้างโปรแกรมหมายถึงการเขียนข้อกำหนดอย่างเป็นทางการซึ่งโดยปกติแล้วจะไม่สามารถนำไปปฏิบัติได้จริง จากนั้นจึงใช้กฎที่ถูกต้องทางคณิตศาสตร์เพื่อสร้าง โปรแกรม ที่สามารถปฏิบัติได้จริงซึ่งตรงตามข้อกำหนดนั้น โปรแกรมที่ได้มาจึงถือว่าถูกต้องโดยโครงสร้าง โปรแกรมและ การพิสูจน์ ความถูกต้องนั้นถูกสร้างขึ้นพร้อมกัน

แนวทางที่ใช้กันโดยทั่วไปในการตรวจสอบอย่างเป็นทางการคือการเขียนโปรแกรมก่อน แล้วจึงพิสูจน์ว่า โปรแกรม นั้นเป็นไปตามข้อกำหนด ที่กำหนดไว้ ปัญหาหลักของวิธีนี้คือ:

• บทพิสูจน์ที่ได้มักจะยาวและซับซ้อน
• ไม่มีข้อมูลเชิงลึกใด ๆ เกี่ยวกับวิธีการพัฒนาโปรแกรมนี้ ดูเหมือนว่ามันจะ "ปรากฏขึ้นอย่างไม่คาดคิด"
• หากโปรแกรมเกิดมีข้อผิดพลาดในรายละเอียดเล็กน้อย การพยายามตรวจสอบข้อผิดพลาดนั้นมักจะใช้เวลานานและแน่นอนว่าจะไม่ได้ผล

การสร้างโปรแกรมแบบสืบทอดพยายามแก้ไขข้อบกพร่องเหล่านี้โดย:

• ช่วยให้การพิสูจน์สั้นลง โดยการพัฒนาสัญลักษณ์ทางคณิตศาสตร์ที่เหมาะสม
• การตัดสินใจด้านการออกแบบโดยการปรับเปลี่ยนรายละเอียดทางเทคนิคอย่างเป็นทางการ

คำศัพท์ที่มีความหมายใกล้เคียงกับการสร้างโปรแกรม ได้แก่ การเขียนโปรแกรมเชิงแปลงรูป การเขียนโปรแกรมเชิงอัลกอริทึม และการเขียนโปรแกรมเชิงอนุมาน

รูปแบบ Bird -Meertensเป็นแนวทางในการสร้างโปรแกรม

แนวทางในการบรรลุความถูกต้องแม่นยำในการประมวลผลแบบกระจายนั้นรวมถึงภาษาวิจัยต่างๆ เช่นภาษาโปรแกรม P

• การตั้งโปรแกรมอัตโนมัติ
• ตรรกะของโฮร์
• การปรับปรุงโปรแกรม
• ออกแบบตามสัญญา
• การสังเคราะห์โปรแกรม
• รหัสการพิสูจน์