Search code examples
mathlanguage-featureslogiclanguage-designlambda-calculus

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 languages 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?

Solution

  • 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.