Either you build the machine, or else you use the machine, because in all other cases you are trying to be the machine

[godelian]

Schooling in mathematics spends a lot of time on:

(1) carrying out arithmetical or algebraic procedures that a tool like wolfram alpha can perform automatically.

-> There is no job where you will ever be required to manually carry out procedures that a computer can carry out.

(2) memorizing proofs

-> Proofs are named after the person who discovered it. That is how rarely it occurs. You won't discover new theorems or proofs by memorizing existing ones. Furthermore, you can only memorize existing proofs because you won't discover them by yourself. If it were that easy, the person who originally came up with it, would not have made it into the history books.

Neither activity is meaningful in any shape or fashion. That is, however, what mathematics education is all about.

[Skepdick]

Schooling in mathematics spends a lot of time on:

(1) carrying out arithmetical or algebraic procedures that a tool like wolfram alpha can perform automatically.

-> There is no job where you will ever be required to manually carry out procedures that a computer can carry out.

(2) memorizing proofs

-> Proofs are named after the person who discovered it. That is how rarely it occurs. You won't discover new theorems or proofs by memorizing existing ones. Furthermore, you can only memorize existing proofs because you won't discover them by yourself. If it were that easy, the person who originally came up with it, would not have made it into the history books.

Neither activity is meaningful in any shape or fashion. That is, however, what mathematics education is all about.

You don't even understand what theorems/proofs are.

https://en.wikipedia.org/wiki/Curry%E2% ... espondence

Rest assured that nobody actually cares about the theorems. Prove them. Don't prove them. You get the noddie badge and maybe some prize. But then a new paradigm of mathematics/research opens up - and everybody flocks to it.

If you are lazy - you can just declare the theorem true.
Or false.

There's your axiom - and now what?

Mathematics is on its way to become formalised/industrialised at which point it's nothing more than sanity-checking of ideas before we implement them in practice.

It's meaningful insofar as you learn how to "compile" software in your head. Compile-time errors are often less costly than run-time errors.

[godelian]

You don't even understand what theorems/proofs are.
https://en.wikipedia.org/wiki/Curry%E2% ... espondence

Concerning CHC. A proof is a program. That is obvious. In all practical terms, a proof can be represented as a script that gets executed by Coq, Isabelle, or any other proof assistant. The execution result is its validity or lack thereof.

The other direction of the CDC, a program is a proof, is not particularly obvious. A correctly terminating script in the Coq or Isabelle proof assistant's language is clearly a proof. However, what does an arbitrary program in, for example, javascript prove?

A converse direction is to use a program to extract a proof, given its correctness—an area of research closely related to proof-carrying code. This is only feasible if the programming language the program is written for is very richly typed: the development of such type systems has been partly motivated by the wish to make the Curry–Howard correspondence practically relevant.

From the above, I can only conclude that most programs are not proofs. In that sense, the notion of "correspondence" in the CDC is a bit misleading.

Mathematics is on its way to become formalised/industrialised at which point it's nothing more than sanity-checking of ideas before we implement them in practice.

In my impression, the vast majority of existing proofs have not been curated to the extent that they all have a corresponding script that runs in Coq or Isabelle.

[Skepdick]

Concerning CHC. A proof is a program. That is obvious. In all practical terms, a proof can be represented as a script that gets executed by Coq, Isabelle, or any other proof assistant. The execution result is its validity or lack thereof.

Not really. Coq/Isabelle guarantee that your theorem is well-defined. If you are getting errors - either it's not well defined; or your proof is incomplete. If you aren't getting errors - it's correct by construction.

This is where the exercise stops. That's what a "program" means in a mathematical sense. The steps of constructing the theorem + its proof.

What you think of as a program is an actual thing you can run on a computer. Sure thing - that's called program derivation/extraction.
Once you've specified it (correctly) you click button - you get source code that works/compiles. Code that corresponds exactly to the Mathematical spec.

https://en.wikipedia.org/wiki/Program_derivation

The other direction of the CDC, a program is a proof, is not particularly obvious. A correctly terminating script in the Coq or Isabelle proof assistant's language is clearly a proof. However, what does an arbitrary program in, for example, javascript prove?

It proves whatever it proves. It has some abstract structure/type - even if you haven't defined it very well.

The entire game is about formalizing the semantics of your code.

And if you don't care - then you don't care.

From the above, I can only conclude that most programs are not proofs. In that sense, the notion of "correspondence" in the CDC is a bit misleading.

Every program is a proof. Some programs are just trivial proofs of mundane things.

Here we are talking about compiler design. If the compiler error-checks your code and it deems it correct: your theorem is good!
It's guaranteed to be structurally sound. It's guaranteed to have zero errors at runtime.

Does this mean it's free of bugs? No. You could've specified the wrong thing. You can't fix logic-bugs with maths.

In my impression, the vast majority of existing proofs have not been curated to the extent that they all have a corresponding script that runs in Coq or Isabelle.

Why would you even want this? It's ludicrously laborious for almost no reward. Unless you are designing mission-critical software where bugs cost lives/billions - it's probably not worth it.

[godelian]

What you think of as a program is an actual thing you can run on a computer. Sure thing - that's called program derivation/extraction.
Once you've specified it (correctly) you click button - you get source code that works/compiles. Code that corresponds exactly to the Mathematical spec.
https://en.wikipedia.org/wiki/Program_derivation

Declarative programs are indeed also programs. The execution engine will indeed have to derive the associated imperative steps. For example, a SQL query is also a program, even though it does not imperatively indicate any steps to follow. In fact, you can still dump the imperative bytecode for something like a SQLite query (https://www.sqlite.org/opcode.html). Coq/Isabelle are in my impression much more complicated virtual machines (execution engines) than SQlite, but they do need to achieve something similar.

The other direction of the CDC, a program is a proof, is not particularly obvious. A correctly terminating script in the Coq or Isabelle proof assistant's language is clearly a proof. However, what does an arbitrary program in, for example, javascript prove?

It proves whatever it proves. It has some abstract structure/type - even if you haven't defined it very well.
The entire game is about formalizing the semantics of your code.
And if you don't care - then you don't care.
Here we are talking about compiler design. If the compiler error-checks your code and it deems it correct: your theorem is good!
It's guaranteed to be structurally sound.

So, in that case, every program always proves something which is usually unspecified and unknown. Well, this is of course always true. But that is not a good thing. Unfalsifiable statements are actually a problem in themselves.

[Flannel Jesus]

Schooling in mathematics spends a lot of time on:

(1) carrying out arithmetical or algebraic procedures that a tool like wolfram alpha can perform automatically.

-> There is no job where you will ever be required to manually carry out procedures that a computer can carry out.

(2) memorizing proofs

-> Proofs are named after the person who discovered it. That is how rarely it occurs. You won't discover new theorems or proofs by memorizing existing ones. Furthermore, you can only memorize existing proofs because you won't discover them by yourself. If it were that easy, the person who originally came up with it, would not have made it into the history books.

Neither activity is meaningful in any shape or fashion. That is, however, what mathematics education is all about.

You sound like you know a lot about how to teach math properly, that's interesting. You have a lot of math education yourself then? A masters or PhD in a math or math adjacent field?

[accelafine]

Schooling in mathematics spends a lot of time on:

(1) carrying out arithmetical or algebraic procedures that a tool like wolfram alpha can perform automatically.

-> There is no job where you will ever be required to manually carry out procedures that a computer can carry out.

(2) memorizing proofs

-> Proofs are named after the person who discovered it. That is how rarely it occurs. You won't discover new theorems or proofs by memorizing existing ones. Furthermore, you can only memorize existing proofs because you won't discover them by yourself. If it were that easy, the person who originally came up with it, would not have made it into the history books.

Neither activity is meaningful in any shape or fashion. That is, however, what mathematics education is all about.

Mr. Proofs discovered proofs? Fancy that. What is his christian name?

[godelian]

You sound like you know a lot about how to teach math properly, that's interesting. You have a lot of math education yourself then? A masters or PhD in a math or math adjacent field?

I did indeed waste my time at university doing a mathematical subject. I spent most of my university days doing operations research. I got my degree before the Bologna declaration in which all EU countries were going to switch to the Anglosaxon nomenclatura of "bachelor" and "masters". So, my degree is still in the old system, which is in between a bachelor and a masters (which did not exist back then).

In fact, most of what I learned in math came much later. It was the result of looking under the hood of things that I was using for my job as well as personal interest. In fact, I never did anything with operations research because it was irrelevant to what I did later on.

Operations research are theories that emerged out of efforts during WWII to streamline the logistics of the allied war efforts. The most important conclusion is that a fully-specified problem can generally not be solved in polynomial time. That is why nobody uses it today. But then again, the math is still very beautiful. It is the math behind a tool like GLPK:

https://www.gnu.org/software/glpk/

The GLPK (GNU Linear Programming Kit) package is intended for solving large-scale linear programming (LP), mixed integer programming (MIP), and other related problems. It is a set of routines written in ANSI C and organized in the form of a callable library.

GLPK supports the GNU MathProg modeling language, which is a subset of the AMPL language.

The GLPK package includes the following main components:

primal and dual simplex methods
primal-dual interior-point method
branch-and-cut method
translator for GNU MathProg
application program interface (API)
stand-alone LP/MIP solver

Of course, we did all the computations manually. So, the university teaches you how to be the GLPK software yourself, only slower and with more bugs.

[Skepdick]

Declarative programs are indeed also programs. The execution engine will indeed have to derive the associated imperative steps.

It can't do that until you actually declare the semantics of the execution engine. It needs to figure out the canonical form of your expression and that is precisely reduction/evaluation.

SELECT * from tableX (all elements of table X)
SELECT * from N (all elements of the natural numbers).

For example, a SQL query is also a program

Sure. You apply SQL query f() to a dataset X. The result is f(X).

You still need to define f() and X.

And you need to make sure that X is NOT the null/empty/bottom/Falsum type.

Coq/Isabelle are in my impression much more complicated virtual machines (execution engines) than SQlite, but they do need to achieve something similar.

They make sure that the "SQL query" (your theorem) doesn't return the empty/null set/bottom type/empty type.

They make sure that the "SQL query" is well-typed (NOT well-defined).

[godelian]

They make sure that the "SQL query" is well-typed (NOT well-defined).

In my impression, the concept of type may look deceivingly simple, but may actually quite difficult to define. In computer languages, we use types like "integer", float, "string", array of some struct, custom-defined class, and so on. Still, what exactly is a type?

A simple definition would be membership of a particular set. For example, integers are members of the set of integers (Z). So, any set membership function could define a type. A set membership function can be implemented as a program. So, in that case a type is just a set for which we can write a program that can act as its membership function.

In fact, I don't see much difference between type theory and set theory. The page below mentions a restriction, but it does not look particularly fundamental:

https://en.wikipedia.org/wiki/Type_theory

Type theory
Differences from set theory

In set theory, an element is not restricted to one set. The element can appear in subsets and unions with other sets. In type theory, terms (generally) belong to only one type. Where a subset would be used, type theory can use a predicate function or use a dependently-typed product type, where each element x is paired with a proof that the subset's property holds for x. Where a union would be used, type theory uses the sum type, which contains new canonical terms.

I really wonder. What is it that you can do with such separate type theory that you would be unable to do with set theory?

[Skepdick]

In my impression, the concept of type may look deceivingly simple, but may actually quite difficult to define. In computer languages, we use types like "integer", float, "string", array of some struct, custom-defined class, and so on. Still, what exactly is a type?

It's a constraint on the domain of discourse. If I tell you that "x" is a variable - I've told you nothing about x. It could be anything.

If I told you that X is a number.... still not very useful.

But if I told you that it's is an integer then you already know what it isn't. It isn't -5, or pi.

A simple definition would be membership of a particular set.

If you don't tell me which set - you may as well not tell me anything. The point is constraint.

For example, integers are members of the set of integers (Z). So, any set membership function could define a type. A set membership function can be implemented as a program.

No, it can't be implemented. Here's a symbol "2" is this a member of N? Is it a member of R? Both?

Suppose X is an integer e.g a member of Z. Is this Z closed or open under division by 2 ?

e.g what's the return type of f(x:Z): return x / 2 ? If you constrain that to integers only then... what's 3/2 ?

Which is basically the same as asking "What's the return type of division?"

So, in that case a type is just a set for which we can write a program that can act as its membership function.

Thus the difference between strongly-typed languages (where the membership of the object is made explicit); and duck-typing/dynamic languages. Where the membership is explicit.

If you are adding integer(2) to real(2) you don't have to do type-casting in a dynamically typed language.

But in a language like Ocaml you do. That's a type error.

In fact, I don't see much difference between type theory and set theory. The page below mentions a restriction, but it does not look particularly fundamental

It's fundamental.

2 + 2.0 is not a valid operation. Until you explain how to cast an integer into a real; or a real into an integer.

I really wonder. What is it that you can do with such separate type theory that you would be unable to do with set theory?

In principle? Nothing. In the same way there's nothing you can do with Assembly programming that you can't do with Agda.

Just gotta be very very very very careful. And specific. And precise. And make sure you check boundary conditions.

[Impenitent]

I got my degree before the Bologna declaration in which all EU countries were going to switch to the Anglosaxon nomenclatura of "bachelor" and "masters". So, my degree is still in the old system, which is in between a bachelor and a masters (which did not exist back then). ...

if it were "not" Bologna, would it be Boolean Bologna?

-Imp

[godelian]

if it were "not" Bologna, would it be Boolean Bologna?

Historically, every EU country had its own nomenclature for degrees and levels. This made degrees across the EU difficult to compare:

https://en.m.wikipedia.org/wiki/Bologna_declaration

The Bologna declaration (in full, Joint Declaration of the European Ministers of Education convened in Bologna on 19 June 1999)[1] is the main guiding document of the Bologna process. It was adopted by ministers of education of 29 European countries at their meeting in Bologna in 1999.

It proposed a European Higher Education Area in which students and graduates could move freely between countries, using prior qualifications in one country as acceptable entry requirements for further study in another.

The principal aims agreed were:

"Adoption of a system of easily readable and comparable degrees". That is to say, countries should adopt common terminology and standards
"Adoption of a system essentially based on two main cycles, undergraduate and graduate. Access to the second cycle [graduate education] shall require successful completion of first cycle lasting a minimum of three years. The degree awarded after the first cycle shall also be relevant to the European labour market as an appropriate level of qualification. The second cycle should lead to the master and/or doctorate degree as in many European countries."

They did not explicitly state in the declaration itself how exactly they were going to harmonize degrees across Europe, but in practice it meant that all countries would adopt the British nomenclature of "bachelor", "master", and "Ph.D".

One consequence is that the old degrees conferred before the harmonization process do not necessarily fit into the new framework. So, now there are people with degrees that are rather partial bachelors or with degrees in between a bachelor and a master. But then again, they are still correctly understood within the individual countries, while they were never understood outside of country anyway. Hence, in my opinion this standardization is actually a good idea.

[Impenitent]

dissolving all cultures into a single mega culture has it's benefits...

erasing certain cultures from the face of the Earth for the sake of "unity"...

being "conquered" and eliminated is simply human history

"welcome to machine"

-Imp

[promethean75]

"if it were "not" Bologna, would it be Boolean Bologna?"

Alright Imp. What's the difference between a Bologna sandwich and a Boolean sandwich?

Go!