Propositions in intuitionistic logic (IL) can be translated into S4 modal logic via the Gödel-McKinsey-Tarski translation.
IL | S4 Modal
A | □A
A ∧ B | □A ∧ □B
A ∨ B | □A ∨ □B
A → B | □(□A → □B)
¬A | □(¬□A)
If you read □ as something like “I can prove that…” then in effect you get the BHK interpretation of IL. BHK is not a ‘system’ just a way of understanding what an intuitionistic proposition is saying. It means that IL has the natural semantics of being the logic of proof or verifiability. By contrast, classical logic (CL) is usually understood as having the natural semantics of truth, i.e. it is concerned with what is the case, whether or not it can be verified. A valid argument in CL can be described as preserving truth, while a valid argument in IL preserves provability or verifiability.
There is no direct connection to natural deduction, since both of these logics can be expressed using it, or for that matter using sequent calculus. CL extends IL by adding the law of the excluded middle (or double negation elimination) and in the case of quantifier logic, by tweaking the quantification rules a little.
The idea that the meaning of a sentence is given by its verification conditions, as opposed to its truth conditions, was a popular one with the logical positivists. It has the consequence that if you don’t know how to verify a sentence then you don’t know its meaning, and by extension, if nobody knows how to verify it, then it is meaningless. This is one way of stating the notorious ‘verification principle’ that the positivists used to claim that much of philosophical language is indeed meaningless.
Positivism fell out of favour for many reasons, not least of which is that it doesn’t really work, although Michael Dummett continued to defend the idea that IL is the ‘correct’ logic and that the semantics of the classical logical constants cannot be justified.
As a rider, it is worth noting that the Curry-Howard correspondence, which relates proof to computability, does extend to CL. So even though CL is normally thought of as non-constructive and IL as constructive, many classical proofs can be extracted as computations. This rather blurs the line between saying that CL is about truth, and IL about provability.