We've been doing this for 200+ years. All the programming languages we use, and mathematical notation, are based in some way upon natural language concepts (yes even FP languages). So really we're talking about a continuum. And also worth noting that human languages evolve over time. So both programming languages will evolve to be more natural, and natural language will evolve to be more machine-parsable.
Yeah. The first time I saw Haskell written out, it felt like a blending of formal math and programming. I was really excited at how it looks like it could have come from my discrete math book. I don't think programming in english is a good idea, but like you said, we will probably get something that looks more like formal languages, because that's what we've always done.
Mathematics as shown in textbooks is not rigorous. I don't understand why so many people fetishize something they saw at university.
Formalised mathematics are incomprehensible to humans and orders of magnitude longer then anything you can see in textbook or mathematical papers outside automated theorem proving.
This reminds me of a tangential rant in the book "The Poincare Conjecture":
"... the postulates are unclear. Does postulate 2 mean that we can extend any line segment forever? Does it mean that we can cut up any segment? And if it means the first, who is to say that the resulting line is unique? And how seriously should we take the definitions? Are they just meant to provide guidance about a word that is essentially undefined (today's, and probably Euclid's, in-terpretation) or are they supposed to completely specify the object named? In the latter case, just what does the phrase "a breadthless length" mean?
Mathematicians and scholars know that there are gaps in Euclid, and there has been a great deal of discussion over the ages about alternate axioms, or possible additional ones. That has not stopped generations of worshipful school-masters, besotted with the majestic order, the accessibility and the patent usefulness of the Elements from rushing in and trumpeting it as the finest in human thought. However, to a thoughtful student, the Elements can seem less rational than capricious. The insistence that the Elements is flawless, and the apex of rigorous thought, turns some students away from mathematics. One wonders how much fear of mathematics stems from the disjuncture between the assertion that Euclid is perfect and some students' intuitive, but difficult to articulate, sense that some things in it are not quite right. Unless you are unusually rebel-lious, it is easy blame yourself and conclude that mathematics is beyond you.
It is worth bearing in mind that mathematical results, for all they are represented as eternal and outside specific human cultures, are in fact transmitted and understood within definite social and cultural contexts. Some argue, for example, that the Greeks invented proof in order to make sense of the statements of mathematical results of Babylon and Egypt without access to the context in which such results were used and discovered. In order to make use of the results, the Greeks needed to sort out different, seemingly..."
We might have different definitions my good sir. Granted I don't have a PhD in math and my math stopped at a masters. To me formalization is theorems and proofs, which are 100% comprehensible to humans. For reference: http://www.vdash.org/formal/#math
Everything in that link looks like programming, especially when you consider something like Haskell. Even formalism as a philosophy tries to add logic to natural language it self. So I am not sure where I am fetishizing what I saw at university. Care to explain without the snark?
Ah I did say they were proofs... that is my fault, what I mean to say is that formalization is the way they are written, is very much a language. Either way. Not sure where the venom was coming from
I never said they were proofs right? I am still confused. I was talking about foramalizing and how at least to me I see programming in it. Even something extremely complex like "The Strong Perfect Graph Theorem" is still readable and reads like english+programming. That's why I said haskell looks like it comes out of a discrete mathbook. I am not sure what your point is or where my fetishization is coming from.
Just to play with the logic a bit. I could see natural language coming up with formal templating to get something closer to a programming language. Not like how we speak will change, but more like how a haiku works is formalized. Similarly to how every CS1 class in university has people who do the "write the steps in making a sandwich" exercise. That exercise is actually easier in a programming language, because of the nature of what a programming language is, its instructions in steps at the end of the day. So perhaps something is formalized that way? Also most modern languages have been slowly adding in things that are easier to read from a natural language perspective VS classical C syntax style. Rust is very C-like but still has plenty of FP like functions built in too.
