Technical Perspective: When Proofs Meet Programs: An Extension of Dependent Type Theory with Church's Thesis

What is a mathematical proof? It can be described as a sequence of logical steps and calculations that serve as evidence of the correctness of a statement. The steps must follow rules that are accepted as correct by the community. One might think there is a set of universal rules. However, this is far from being the case.