[leonidasrup]

Constructing a formal proof is not only related to programming, it's the same thing. Curry–Howard correspondence:

"In programming language theory and proof theory, the Curry–Howard correspondence is a direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation."

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[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).