[still_grokking]

I think you're missed the elephant in the room.

"Programs as proves" is only a thing in the context of mathematically pure languages.

Almost all programming languages aren't pure.

That's on the other hand's side why prove assistants are very unusable as programming languages; you can't do anything with them usually besides proving stuff. Running actually "useful" code is mostly not possible. Things like Haskell or Idris try to bridge both worlds, but this isn't straight forward. How to actually do anything in a pure programing language is still an open question. Monads are some kludge but not very practicable for most people…

So to summarize: "Normal" programs don't correspond to proves in any way!

[peter_d_sherman]

You might wish to have a look at "Propositions as Types" by Philip Wadler (thanks rbonvall, for the link!) -- at 21:30 (1290 seconds) into the video:

https://youtu.be/IOiZatlZtGU?t=1290

"Evaluation corresponds exactly to simplification of proofs..."

(The rest of the video, both before and after this statement, contain more context...)

That being said, I agree with you that languages which are used primarily for theorem proving (AKA, "proof assistants") -- are usually not as applicable to as broad a range of programming paradigms and problems as most general purpose computer programming languages are...

[still_grokking]

You might wish to re-watch the linked talk as you just restated your confusion (which was already the cause of a lot of down-votes in this thread).

Wadler says there:

"Evaluation [of simply typed lambda calculus!] corresponds exactly to simplification of proofs…"

If you didn't get that context you actually missed the whole talk.

You really need to understand: "Programs as proves" is only a thing in languages with strongly normalizing type-systems. This implies that the language is pure and does not contain general recursion.

In a language with mutation (which is obviously not pure) you can destroy any "prove" by just writing to a variable, e.g. switching a single bit in the case of a boolean value.

Terms can be obviously only proves if it's not possible to change a term ("prove") form true to false (or the other way around) at will! Once some term is determined as having some type it may not change any more. This rules out obviously any language with mutation or I/O.

That's why you can't write applications in Agda, or mathematical proves in Haskell. (In the general case; you could do both with "tricks"; but those are indeed tricks).

[peter_d_sherman]

>"Programs as proves" is only a thing in the context of mathematically pure languages.

>Almost all programming languages aren't pure.

Yes, but any Turing-Complete language -- is Turing-Complete...

Challenge: Show me a Mathematical Algorithm -- that can be expressed in Math, that cannot be expressed using symbols and symbol manipulation on a Turing Machine -- that is, on any plain, regular computer...

Hint: Every computer that Mathematica runs on -- is a Turing Machine...

Extra Hint: Mathematica can express, manipulate (and typically solve!) -- any expression in Mathematics...

Extra Extra Hint: Programming Languages need not be "pure" -- to be Turing-Complete.

[still_grokking]

You have again mixed up quite some things here.

It's getting tedious to be honest…

Your question is trivial anyway: An algorithm is something that can be performed by a (Turing-complete) machine.

Therefore there exists no algorithm that can't be computed (on a Turing machine). That's by definition!

But this has absolutely nothing to do with which kinds of languages can be used to prove anything in math.

To prove something you need algorithms that are guarantied to produce results. Your machine must halt to spit out a result!

But as everybody knows there is no such guaranty for arbitrary algorithms. The question whether some arbitrary algorithm halts is undecidable.

Therefore Turing-complete languages are "too powerful" to be used to prove things. Because you can't know whether a "prove" in such language can be computed at all.

Or to formulate it differently: A computer can't compute uncomputable numbers, or decide undecidable problems.

But math can—of course—express uncomputable numbers. (I hope you're able to google some definitions of such number on your own…)

And just a reminder: This site is not the right place to learn basics.

Also your tone is getting unacceptable.

That said, please keep in mind that the internet does not forget… Your childish behavior will be remembered until the end of time. (In case you've forgot, you're posting here under your RL name, boy.)

[peter_d_sherman]

>An algorithm is something that can be performed by a (Turing-complete) machine.

We agree so far...

>Therefore there exists no algorithm that can't be computed (on a Turing machine). That's by definition!

We agree so far...

>But this has absolutely nothing to do with which kinds of languages can be used to prove anything in math.

Here we disagree!

It has everything to do with which kinds of languages can prove anything in math!

If a language is Turing-complete, it can run any algorithm.

If a language can run any algorithm, it can be programmed to perform symbolic manipulations of Math equations that are expressed in symbolic form.

Basically, it can perform Mathematics.

This is what Mathematica is and does.

Mathematica could be programmed -- in any Turing-complete programming language.

If Mathematica could be programmed in any Turing-complete programming language, and Mathematica can be used to solve any Mathematical problem, then any Turing-complete programming language could be used to program what Mathematica does -- which is Mathematics, basically.

Which includes Mathematical proofs, incidentally.

>Your machine must halt to spit out a result!

This is a contradiction. Functions (and Programs) -- do not need to halt to spit out a result.

>The question whether some arbitrary algorithm halts is undecidable.

Algorithms (and programs and functions!) -- can be tested for halting by actually running them!

If they halt, they halt (99.9999% of them do not -- unless they are coded wrong!)...

>Or to formulate it differently: A computer can't compute uncomputable numbers >or decide undecidable problems.

Yes -- but this reframes all mathematical proofs as being uncomputable and/or undecidable.

Challenge: Show me a mathematical proof which is either uncomputable and/or undecidable.

>But math can—of course—express uncomputable numbers. (I hope you're able to google some definitions of such number on your own…)

Computers can express uncomputable numbers (and any other concept in Mathematics) symbolically.

Computers can express proofs (and other operations in Mathematics) via symbol manipulation.

This is what Mathematica does.

Variables, after all, are symbols.

They can be symbols of things in the real world and/or they can be symbols of ideas...

But any symbol if defined in a Turing-machine, by whatever method -- can be symbolically manipulated in that Turing-machine.

Any language which is Turing-complete -- has the ability to manipulate symbols in this way -- if properly programmed -- like Mathematica does...

Conclusion: All Turing-complete programming languages -- have the ability to express Mathematical proofs, like Mathematica does, if properly programmed to do so...

>Also your tone is getting unacceptable.

To who, exactly?

?

Perhaps pure logic is interpreted as "tone" -- but the error of that particular type of interpretation -- is not on my side of the fence! <g>

>That said, please keep in mind that the internet does not forget… Your childish behavior will be remembered until the end of time.

I hope it does! <g>

The Internet will remember me (for a long time!) -- for my dedication to self-evident truths, first principles, logic, reason, clear thinking and simple explanations...<g>

The Internet, on the other hand, tends to forget people who endlessly confuse, distract, complain, propagandize, derail, make mountains out of molehills (and molehills out of mountains!), speak with "forked tongues" and engage in Selective Abstraction, Arbitrary Inference, Equivocation, Prevarication, Duplicity, Straw Man arguments, Dichotomous Reasoning -- or one/some/all of the above!

I'm not saying that that's you...

I'm just saying that the Internet tends to forget such people... <g>

You know, I guess it's their "right to be forgotten" -- for one or more such activities! <g>

>(In case you've forgot, you're posting here under your RL name, boy.)

<g>

Well, we know for a fact that I am neither:

a) A GPT-3 or other bot...

b) A paid disinformant and/or Troll...

c) Someone with such a large degree of narcissism and/or agenda -- that they feel the necessity to continuously railroad other posters to their point of view (remember, you engaged me in conversation first -- I did not engage you!)

d) One/Some/All of the above...

>And just a reminder: This site is not the right place to learn basics.

No site on the Internet is the right place to make illogical arguments to logical people...<g>