Relating a proof to a Haskell program

I am trying to relate the following integer square root theorem

$\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$

and its proof to its role as a specification of the Integer Square Root isqrt ($\lfloor \sqrt{x} \rfloor$) function in a Haskell program.

Below is a inductive proof of the theorem and the related Haskell program.
The proof was done using natural deduction in the Fitch system, hence there are notational differences between code and proof e.g. no $\leq$ in Fitch.

For my question the details of the proof are not important. I wish to focus on the base case, and the two cases involving $\exists$-Elimination and $\lor$-Elimination.

I used Quickcheck as a reasonable check that the theorem holds in the code.

I can see that cases 1 and 2 in the proof correspond to the guard conditions in the Haskell definition of isqrt function. I did not specify, prove, and implement the function isqrt in any structured way. I just used any examples I could find. I believe that there must some more formal transformation from proof to code that I am missing. So despite having written both the proof and code the precise correspondence between both eludes my comprehension.

Is there a technical name for this form of proof to program relation?
I would be grateful for an explanation or pointer to the literature.

module Peano where
import Test.QuickCheck

data Nat = Z | S Nat deriving Show
-- addition
(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)
-- multiplication
(*@) :: Nat -> Nat -> Nat
x *@ Z = Z 
x *@ S y = (x *@ y) +@ x 
-- square
sqr x = x *@ x 
-- equality
(=@) :: Nat -> Nat -> Bool
Z =@ Z  = True
(S m) =@  (S n) = m =@ n 
_=@ _  = False 

-- lesst than
( Nat -> Bool
Z  Nat -> Bool
x   arbitrary) ]

isqrtPostCondition :: Nat  -> Bool
isqrtPostCondition x  = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.

Your goal is to “prove” --I'm using bullets “•” for syntactic separators--
$$ ∀x \;•\;\; ∃y \;•\;\; y² ≤ x

-
To reach our goal (*), let's do the simplest thing possible:
replace $a$ with $S a$ in (1) thereby obtaining
$b² ≤ S a

-
So if this is true, then we are done and the answer is $b$.

-
If it is not true, then we must have it complement:
$$(b + 1)² ≤ S a$$

-
But from (1) we also have $a

-
Hence, we have found that $(b + 1)² ≤ S a

Curry-Howard: Proving ≅ Programming

The above was a proof [sketch] which corresponds to the a program.

A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$
corresponds to the program

-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0  = “the y found in the base case of the proof”
prog n  = “the y found in the inductive step, 
             along with any conditionals and recursive calls”

Applying this to our above proof yields,

prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
         in
           if   a + 1 <= (b + 1) * (b + 1)
           then b
           else b + 1

Hope that helps :-)

StackExchange Computer Science Q#97637, answer score: 5