[jroesch]

Language choice can be important. If you do the common thing and build a distinct model of your program and prove it correct your guarantees don't hold about the actual implementation. You need a second method to ensure equivalence between your model and implementation, this obviously requires much more work and can vary greatly based on the tools and programming languages involved.

[jude-]

Yes--choose the language and development process that makes it easiest to reason about the desired properties of the program.

Example: seL4 is written in C (as in, written by hand by fallible humans--not compiled down from a higher-level language [1]). But, the C is written in such a way that it is feasible to prove its equivalence to a Haskell prototype which had previously been proven correct.

Yes, language choice can be important. But, the degree of its importance depends on what you're building with it and how you're using it.

[1] http://www.nicta.com.au/pub-download/full/7371