Relating a proof to a Haskell program

Question

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 -> Nat -> Bool
Z <@ Z = False 
Z <@ x | not(x =@ Z) = True 
x <@ Z | not(x =@ Z) = False 
(S x) <@ (S y) = x <@ y 


-- less than or equal
(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False


-- Integer square root function
isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@  (S x) = (S (isqrt x))
            | (S x) <@ (sqr (S (isqrt x))) = isqrt x

-- test with Quickcheck
instance Arbitrary Nat where
 arbitrary = oneof [return Z, (S  <$>  arbitrary) ]

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