1) functional programming is a subset of mathematical proofs. Isabelle syntax is somewhat similar to what is offered in ML family of functional languages. Unlike functional languages, you can use more advanced constructs than bijections (can model superposition etc.) and it is easier to state things over sets.
2) imperative code is a subset to this too with added order of operations. Language is somewhat different though Isabelle has a module that has necessary proofs to verify imperative programs.
1) functional programming is a subset of mathematical proofs. Isabelle syntax is somewhat similar to what is offered in ML family of functional languages. Unlike functional languages, you can use more advanced constructs than bijections (can model superposition etc.) and it is easier to state things over sets.
2) imperative code is a subset to this too with added order of operations. Language is somewhat different though Isabelle has a module that has necessary proofs to verify imperative programs.