So how can we put this to practical use to describe (functional) programs written in practical programming languages like say Lisp or JavaScript or even Haskell?

I assume that would require having some additional notation for built-in concepts like Numbers for instance, and built-in named library functions ?