By this token, everyone who counts apples in a market is using the axioms of Peano arithmetic every day.

The fact that our high level languages compile down to assembly doesn't mean we use assembly in any meaningful sense. My C code will be correct or not based on whether it conforms to the semantics of the C abstract machine, regardless of whether those semantics match the semantics of the assembly language that it happens to compile down to. Even worse, code that is perfectly valid in assembler may be invalid C, even if the C code compiles down to that same assembler code. The most clear example is adding 1 to an int variable that happens to have the value MAX_INT. This code will often compile down to "add, ax, 1" and set the variable to MIN_INT, but it is nevertheless invalid C code and the compiler will assume this value is impossible to happen.

This relationship between a programming language and assembler is even more tenuous for languages designed to run on heavy runtimes, like Java or JavaScript.