Convergence of Mathematics and Programming Languages

Question

It seems that there is a strong movement for converging the languages ​​of mathematics and computer programming, which, in particular, is evidenced by the influence of the lambda calculus on modern languages. Most of the time I don’t think with math, I think with logic. It seems to me that many of the phenomena that can be mathematically modeled can also be modeled logically.

I don’t think that we will ever see a purely logical language or a purely mathematical strengthening of a language for general-purpose programming, but I would like to take an inventory of the advantages of each paradigm. I'd like to know:

• What are the advantages of modeling programming languages ​​or language functions in mathematics?
• What are the advantages of language modeling on the principles of formal logic?
• Can a general-purpose language undergo logic or math?
• What are some of the languages ​​that truly demonstrate the benefits of any approach?
• What hardware features make one approach more attractive than another?

Answer 1

First of all, I do not see a big difference between logic and mathematics; the latter has just been systematically applied to specific structures.

Also, I'm not sure that the theoretical beauty of programming languages ​​based on math / logic is really worth it to succeed by writing effective, supported code.

Regarding specific issues.

What are the benefits of modeling programming languages ​​or function language in math? What are the benefits of language modeling using formal logic?

Proofs of correctness become much simpler - although it is doubtful whether we will ever get to the point where they become practical for real systems.

Can a general-purpose language betray either logic or mathematics?

Depends on what you mean by "forgo". You can have a language without mathematical operations (although you should get pretty multi-ethnic, Turing machines are the only thing I can think of that doesn't even have an increment or decrease), and you can certainly have one that doesn't care on formalisms (Assembler, C). But I do not think it is possible to have a programming language without logic (although it may be perverse logic, cf. Malbolge )

What are some of the languages ​​that truly demonstrate the benefits of any approach?

Well, if you think that lambda calculus is a form of logic, then Lisp demonstrates its advantages well, since since 1958, a language into which expressive power expresses other languages ​​(but does not cope) has reached.

Then there is Prolog, the only other “serious” language that I know, which is trying to be clearly substantiated in formal logic. And - quelle surprise - it's good at logic and a bit more.

What hardware features make one approach more attractive than another?

Missing. The failure of Lisp Machines proves IMO quite convincingly that compilers + general hardware are more powerful than specialized hardware. However, it can be said that the simulative power of today's system makes languages ​​that completely ignore hardware limitations practical where they were not before.

Answer 2

since computer science is a special branch of mathematics, there is no convergence of mathematics and programming language. In a programming language, mathematics is used. This is a tool created by people with a deep knowledge of mathematics that will be used by others (in most cases with less deep knowledge). You can compare it with a light switch - you can use it without studying physics, but physics is used. Sometimes (especially if you have a problem), you need to have "knowledge." Then you need a special background.

Answer 3

Well, to be honest, many of these so-called “modern programming languages” are just experiencing things that have been in different programming languages ​​for over 50 years.

Answer 4

What are the advantages of modeling programming languages ​​or language functions in mathematics? What are the benefits of language modeling using formal logic?

This is one and the same thing: formal logic is just a branch of mathematics. The two main advantages of using formal mathematics are optimization and security. When an algorithm has no side effects (i.e., is referentially transparent) and is expressed exclusively using pure mathematicians, compilers can restructure the algorithm in accordance with the rules of mathematics. This makes it easier for compilers to optimize code and use parallel architectures. Another important advantage is the ability to prove certain properties of the code.

Can a general-purpose language betray either logic or mathematics?

Not. How would you perform logical operations or arithmetic without logic or math. You can mean something here that I do not understand.

What are some of the languages ​​that truly demonstrate the benefits of any approach?

Haskell, ML, OCaML, Miranda, Alice, Oz, Erlang, Twelf, Coq, Prolog, all demonstrate more rigorous applications of mathematics for programming.

What hardware features make one approach more attractive than another?

I do not believe that hardware changes much in terms of the benefits of rigorous mathematical programming approaches. The benefits of link-transparent code are mostly at the compiler level.