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.
