Convergence of Mathematics and Programming Languages

It seems that there is a strong movement for the convergence of mathematics and computer programming languages, this is notably evidenced by the influence of the lambda calculus on modern languages. Most of the time I do not think with mathematics, I think with logic. It seems to me that many of the phenomenon that can be modeled mathematically can be modeled logically as well.

I don't think that we'll ever see a purely logical language or a purely mathematical language gain traction for general purpose programming, but I'd like to take an inventory of the benefits of each paradigm. I'd like to know:

• What are the benefits of modeling programming lan开发者_高级运维guages or language features on mathematics?
• What are the benefits of modeling a language on the principles of formal logic?
• Can a general purpose language forgo either logic or mathematics?
• What are some of languages that really show off the benefits of either approach?
• What hardware features make one approach more attractive than the other?

First of all, I don't see much distinction between logic and mathematics; the latter is just the former applied systematically to specific constructs.

Additionally, I am not convinced that the theoretical beauty of programming languages grounded in math/logic is really worth much when it comes to getting things done by writing efficient, maintainable code.

As for you specific questions.

What are the benefits of modeling programming languages or language features on mathematics? What are the benefits of modeling a language on the principles of formal logic?

Proofs of correctness become much easier - though it's questionable whether we'll ever get to the point where they become practical for real-life systems.

Can a general purpose language forgo either logic or mathematics?

Depends on what you mean with "forgo". You can have a language without mathematical operations (though you have to get pretty esotheric; Turing machines are the only one I can think of that doesn't even have increment or decrement), and you can certainly have one that cares nothing about formalisms (Assembler, C). But I don't think it's possible to have a programming language without logic (although it may be a perverted logic, cf. Malbolge)

What are some of languages that really show off the benefits of either approach?

Well, if you consider Lambda calculus a form of logic, then Lisp has been showing off its benefits pretty well by being since 1958 the language whose expressive power other language aspire (but do not manage) to reach.

Then there's Prolog, the only other "serious" language I know that tries to be explicitly grounded in formal logic. And - quelle surprise - it's good at logic stuff and little else.

What hardware features make one approach more attractive than the other?

None. The failure of Lisp Machines proves IMO pretty conclusively that compilers+general hardware are more powerful than specialized hardware. However, one might say that the simpe brute power of today's system are making languages that completely ignore hardware constraints practical where they previously were not.

since computer science is a special branche of math - there is no convergence of math and programming language. A programming language is applied math. It's a tool created by people with profound knowlege of math to be used by others (most of the time with less profound knowledge). You can compare it to a light switch - you can use it without having studied physics but still it is applied physics. Sometimes (especially if you have a problem) it is necessary to have the "knowledge". Then you need the special background.

Well, to be honest a lot of these so-called "modern programming languages" are just imlpementing things that have been in various programming languages for over 50 years.

What are the benefits of modeling programming languages or language features on mathematics? What are the benefits of modeling a language on the principles of formal logic?

These are the same thing: formal logic is just a branch of mathematics. Two major benefits of using formal mathematics are optimization and safety. When an algorithm has no side-effects (i.e. referentially transparent), and is expressed solely using pure mathematics compilers can restructure the algorithm according to rules of math. This makes it easier for compilers to optimize code and to exploit parallel architectures. Another important benefit is the ability to prove certain properties of code.

Can a general purpose language forgo either logic or mathematics?

No. How would you do boolean operations or arithmetic without logic or mathematics. You may mean something here that I do not understand.

What are some of languages that really show off the benefits of either approach?

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

What hardware features make one approach more attractive than the other?

I don't believe the hardware changes things much in terms of the benefits of rigorous mathematical approaches to programming. The benefits of referentially transparent code are mostly at the level of the compiler.