[layer8]

It’s not the same thing, in particular if you work in a dynamically-typed programming language, have mutable state, parallelism, and infinite loops. The Curry–Howard correspondence only applies in a limited sense to practical programs.

That’s why you can have a productive programmer who is nevertheless unable to construct valid proofs.

(I’m very much in favor that programming should involve proofs as much as possible, but that’s something to strive for, not a matter of fact.)

[lioeters]

The Curry-Howard correspondence applies to all programs and computation, regardless of language. Some languages, such as dynamically typed ones, expose only a higher level abstraction where its inner workings are implicit and hidden (that's the trade-off), so the user of the language cannot work with the actual fundamentals.

[deterministic]

Not true. seL4 (for example) is an example of a real time kernel proven correct end-to-end and used on millions of devices.

Another example is CompCert (a proven correct C compiler used by Airbus and others for real production software).