The trust you place is based on mathematical evidence for the soundness of the compiler. The compiler is thus trustworthy, based on formal arguments, as opposed to informal arguments (such as "we did some testing" or "no bugs are were reported").
Going back to Kant, formal arguments in this sense are a priori knowledge -- knowledge that is in some sense objective, and independent from any observer making empirical measurements (as opposed to a posteriori, or experimental, knowledge).
Thanks. My school's CS department was very strong in theory, among other things, and so there were a lot of very mathy people in the program mixed in with the more practical proles. Most of them were very nice, but there was something of a communication problem because (I assume) they were too naturally talented at such things to be able to explain them very well. I remember one guy who would get this look of satisfaction on his face every time a teacher would start talking about formalisms, as if he were eating his favorite food, or sitting down after a long day on his feet, and that's my first association with the word "formal" in a CS context.
A little bit of explanation about formalisms and the communication problems you mention from a computer scientist/linguist who gets that same look of satisfaction:
In natural languages, the relationships between utterances and what they convey are somewhat fuzzy. Words like "tree" and "run" don't have single precise meanings; they have a variety of senses associated with them, and these senses vary in how closely they are related to each other. Biological trees made of cells are quite closely related to computer science trees by their shared shape; the relation between running with your legs and running for office is a bit fuzzier, via the race metaphor; the relation between a river bank and a financial bank is even more unclear.
Meaning in natural language is built in aggregate from associations, with the senses of expressions converging over time in groups of communicating speakers. Natural languages do not clearly define the relationships between different expressions, nor between expressions and the real world. Because natural languages are unspecified and evolving, you can only measure how often (in your observation) different expressions and relationships between expression reflect different situations.
Formalisms, like natural langauges, are also used to represent meaning via expressions made of symbols and relationships between them. (Technically, formalisms don't have to represent anything, but in practice they usually do because otherwise they're not very useful.) Unlike natural languages, formal languages have normatively defined specifications. These specifications can be written in a variety of ways, but usually they define rules (which always apply) for deriving expressions from each other.
To be able to use formal languages for real-life problems, you need to have these five skills:
Symbol manipulation: deriving expression in desirable forms from old ones using a specification
Interpretation: relating formal expression to the domain
Encoding: capturing domain knowledge in the formal language
Abstraction: finding consistent patterns in the domain (to be expressed in the formalism)
Modeling: expressing relationships in the domain using relationships between symbols
Unfortunately, most people are not very good at these skills. It is hard to break habits like using intuition and relying on others' ability to resolve ambiguity. Furthermore, most people are not very good at dealing with abstractions, especially new ones or higher-level ones. To make things worse, some of the problems involved in using formal systems are genuinely hard, even for computers and mathematicians. Obviously, even the most accomplished mathematicians are not always able to get the results they are looking for, let alone quickly, but people who are good with formalisms usually don't have as many problems with things like checking their intuition or dealing with abstractions.
The problem with communicating formal ideas to people who are not good with formalisms is rather fundamental, because the very attributes which make formalisms useful are the ones that those people have trouble understanding. You can, of course, relate the results of using a formalism, but without using formalisms it is often very hard to usefully express the "why" of the result. The problem is compounded because people who are good with formalisms have a hard time figuring out what is understandable to others, due to the general "knowing it too well to teach it" effect as well as lack of practice (since most people who care about formalisms are good with them).
Some talented communicators are able to explain formal results satisfactorily to others by relating them to familiar abstractions or rephrasing their logic in everyday terms, but unfortunately this frequently results in misunderstanding and misapplication of the results. Furthermore, there are a number of formal results which really can't be properly understood unless you have mastered the skills above (particularly in theoretical computer science and formal logic). The problem is akin to trying to talk to non-programmers about programming, but more general. Programming languages are formal languages, of a sort, but most programmers only understand a few particular formalisms. Theoretical computer science and proof theory involve dealing with a larger and more abstract set of formalisms, including formalisms about formalisms.
If you need examples of the difficulties, just look at all the ways that people try to explain Gödel's incompleteness theorems or monads informally.
