5 ms·

Why do this rather then define an abstract, human-evaluatable, programming language? Give it some S-expr syntax and make more things implicit and you're golden.

Why do this rather then define an abstract, human-evaluatable, programming language? Give it some S-expr syntax and make more things implicit and you're golden. Making strange squigles on a page doesn't help. Making strange greek symbols on the page doesn't help. Writing functions, "unit tests", building on abstractions, and creating "libraries" do help. We all know this because it works well in CS. Why would this not work well in physics? Ditch the alphabet soup (and yes, even the 5th centry Greek alphabet soupe). Abstract common ideas into "functions". Write human-provable "test-cases". Add documentation. Use logically derived variable names (even if they're 5-10 characters). Formalize the definitions and syntax of this language and it's abilities. You'd be golden. Phi shouldn't mean 30 things depending on the field you're in. Am I wrong? Is this not possible? Is there a reason as to why math and logic can't be expressed as an abstract programing language? Is there a reason why it wouldn't be better to have a completely standard way as to how to define all of your algorithms and logical assertions? I could be wrong but no one has provided information as to why what we do is better. Nor does this look much better (what kmill has linked).

doubleunplussed 10y ago
When you write a function, you still need to give the arguments names. When you write an algorithm and want to share it with someone, you still need to give the variables names. That's all the greek symbols are - and mathematical notation is an abstract, human evaluateable programming language. Common ideas are abstracted into functions, like sine, cosine - min, max, even weird things like Bessel functions, Legendre polynomials, these are all written as function(arguments) in maths. Maths has indexing, a bunch of operators, and what the operators do often depends on what type of objects they're applying to. Python's list and set comprehensions etc actually come from a real mathematical notation for defining sets. All those capital sigmas and capital pi's are reduction operators - sums and products. There isn't an assignment operator - you're expected to give each variable a unique name if you have a multi-stage process, so you only ever make statements of equality rather than assignment. Sure, it's an ambiguous language sometimes, but it sounds like your complaint comes down to standardising it more and using longer variable names.
- gravypod 10y ago
  > Sure, it's an ambiguous language sometimes, but it sounds like your complaint comes down to standardising it more and using longer variable names. Has unstandardization and shorter variable names ever been heralded as the icon of understandability? I think that answers how I feel about that. > When you write a function, you still need to give the arguments names. When you write an algorithm and want to share it with someone, you still need to give the variables names. That's all the greek symbols are - and mathematical notation is an abstract, human evaluateable programming language. I get that. When I write a loop over a space of integers I sometimes use "i" or "j". When I iterate over a 2d array I usually use "x" and "y" ("z" for 3d). If I'm writing networking/file code I usually have an array of N length of bytes called "buff" or "buffer". These are all common threads. But when I'm writing "buffer", "i", "j", "x", "y", or "z" they mean the same thing at every location in every piece of software to every software developer. But, and here's the big but, I get a tingling feeling every time I use one of these. I always ask myself "is this the meaning I'm attempting to convey"? If there's a slight variation I'll just rename the variable to a more verbose version to make it easier to follow. > Common ideas are abstracted into functions, like sine, cosine - min, max, even weird things like Bessel functions, Legendre polynomials, these are all written as function(arguments) in maths. I can't name an idea in computer science that isn't a function (in at least 1 major programming language). We can go so far as to say that the basic operators, right down to define, are functions in LISP. I can on the other hand name many ideas that aren't functions in "Math"-lang and I'm sure you can as well. > Python's list and set comprehensions etc actually come from a real mathematical notation for defining sets. The difference is python uses, for the most part, the ASCII character set and presents a simple-for-all notation. > All those capital sigmas and capital pi's are reduction operators - sums and products. Why does Pi and Sigma provide a better interface to these operations then apply and reduction notation of LISP? > There isn't an assignment operator - you're expected to give each variable a unique name if you have a multi-stage process, so you only ever make statements of equality rather than assignment. Am I just supposed to guess the starting state of a variable? How do I define variables based on others? What type is my new variable (collection, graph, tree, value)? Why not just have a simple variable name for every non-common variable (Pi for Pi or 3.14... is fine because it is a constant everywhere). Also, if there is a multi-stage process you should have multiple functions that define a subset of the solution, each with an appropriate name, each with appropriate "test-cases" (proofs) for that subset, each with documentation and type annotations to provide an understanding as to how it works. None of them should require domain-specific ideas to understand after you've read the "tests", docs, types, and names.
throwaway729 10y ago
> Am I wrong? Is this not possible? Yes, you're wrong. I mean, I agree with you. This is the route we should commit to. Building up mathematical theories in a programming language. But I think you've reached the right conclusion for horribly confused reasons, and that you severely over-estimate the state of the art in CS. This over-estimation results in you not realizing why something like this could be a valuable tool within the world you describe. Perhaps I'm wrong, but here's what gives me this impression: > Write human-provable "test-cases" Since the article is discussing mathematics, I suppose here by proof you actually really honestly mean proof. So proof by "I worked through 6 examples and they all turned out OK so far"? That's not typically what a mathematician means when they say they proved something. Proofs can get horribly complicated in ways that test cases generally don't. > Writing functions, "unit tests", building on abstractions, and creating "libraries" do help. We all know this because it works well in CS. Yes, all of these things would be great. But it's REALLY not that simple. Formal verification of software systems remains a mostly academic pursuit. There's some promising early work, but almost none of "us" formally verify our software. It does NOT work well in CS. Not at the moment. And most things we do in CS are conceptually simpler than a lot of mathematics. So exploring alternative interfaces makes a lot of sense. > Is this not possible? Is there a reason as to why math and logic can't be expressed as an abstract programing language? They can be. It's horrendously verbose, and it's difficult to do novel work in such a formal setting. It does not work well in the same sense that it does not work well in CS -- you can do it, if you're willing to spend 10x the time/money/effort for the "good enough" version (in math, paper proofs; in CS, shippable but unverified code).
- gravypod 10y ago
  > I think the problem is that you don't understand what a real result looks like in math Unfortunetly I've been plauged with the task of reading some math papers to understand some things in the past. I still wake up in a cold sweat some times. > So proof by "I worked through 6 examples and they all turned out OK so far"? > That's not typically what a mathematician means when they say they proved something... I'm well aware. That's why I included the quote marks. I mean a logical proof based on the relation of this "function's" suppositions in relation to the rest of the "functions" it is integrated with providing context and mathematical relations to the other parts of the conjecture you're working on. > Formal verification of software systems remains a mostly academic pursuit. There's some promising early work, but almost none of "us" formally verify our software. > So no, you're wrong. It does NOT work well in CS. Not at the moment. I mean this is just blatantly wrong and ignoring the face of what I'm saying. I'm implying that 1) if you have a pinical example of computer science you can take a freshman-level CS student, give them a tour of the language, and let them loose on a problem and they'll understand what's going on. Some of the worlds most complex simulation sytems have children in highschool writing games in them. Things like Unity and Unreal engine representing thousands and thousands of manhours to create along with entire libraries of research, industry-funded experiments, and years of expertise. I'm saying that the common practices of programming can yield systems that are simple for anyone to maintain and work on. I can't say the same for mathematics. While I understand the concepts of derivatives, integrals, and calculus if tasked I'd most likely not be able to provide a formula to define the area of a new shape despite understanding the core material far better then most programmers understand the new project they've been flung into. 2) the concepts from computer science and programming can be adapted to suit math's needs and these adaptations can be fluid where novel augmentations of the processes that yield positive results can be further integrated into mathematics. Programming and computer science are quickly evolving fields and have a unique possition in that many people engage in them without formal training from a university because in most cases it's simple unneeded. You can pick up one book and then rely on the common goal of every computer scientist and programmer that came before you: abstraction of the concepts to yield a simple solution to arbitrarily complex problems. Because of this you can jump anywhere and pick up and run with your work. I'm not saying these ideas are directly applicable with no modification. What I am saying is "these are the ideas that make my field possible" and suggesting that standardizing practices in the Math-heavy fields would not be a bad thing especially if these same standardized practices have been used to great lengths in our field to produce a set of very positive outcomes.
lend000 10y ago
The plethora of Greek symbols and italicized fonts for fancy operations make interesting research papers mostly unreadable for me. It would be great if mathematicians started using descriptive names for each variable (including non-obvious functions/operations), and weren't limited to one letter per symbol (i.e. I'm describing programming). Granted, there's too much momentum to change anything, especially since it would probably slow down the people doing the fancy math.
- klodolph 10y ago
  It's not just momentum. "Non-obvious" is relative. Every mathematical paper is built on top of thousands of pieces of foundational work, how do you pick which pieces of the foundation are obvious and which are non-obvious? And how do we even use descriptive names? Descriptive names were used in older works like Philosophiæ Naturalis Principia Mathematica which are practically unreadable (even when translated into your native language) compared to more modern ways of writing things like "F=ma", "F=mx''", or "F=m d^2x/dt^2", which are fantastic to understand. Or if I'm writing something like "x+0=x", is there really some descriptive name I can use for "x"? Or in short, we tried that and terse notation tends to be both easier to understand and more concise.
andrepd 10y ago
I have absolutely no idea what you're trying to say. What do you mean with all that? Maybe I'm being obtuse but you're just saying random words and terms from programming. How on earth is that applicable to physics? I have absolutely no idea what you're trying to propose.
- gravypod 10y ago
  The incorperation of broader programming principles and concepts that have evolved over the course of advancements in the creation of software systerms into other language-based fields including mathematics and standardization of these languages to lessen ambiguities. Things like using variable names that make sense rather then the current single-letter + subscript limit. Using easily typable characters and combining those to create complex operations. Substituting language for obtuse symbols. Simplification of expression syntax. I don't know best how to put it in your terms, nor what I'm missing, because these are things I take for granted being a programmer.
- traverseda 10y ago
  Well, not OP, but that was all very understandable to me, and resonated. I'll try to explain some specific points. >Why do this rather then define an abstract, human-evaluatable, programming language? The syntax of math is bad for a number of reasons. Making it some big 3D thing isn't going to make that syntax more reasonable. Math is a language that could learn a lot from programming languages, even if you don't plan on running it on a computer and dealing with all that hassle. >Making strange squigles on a page doesn't help. Making strange greek symbols on the page doesn't help. >Ditch the alphabet soup (and yes, even the 5th centry Greek alphabet soupe) Math is optimized for paper. This makes it a lot less accessible these days. All these custom glyphs are a damn weird idea. Naming your variables "a" wouldn't be accepted in any other languages. >Abstract common ideas into "functions". Once you've abandoned the idea of single-letter variable names, it becomes easier to abstract common mathematical ideas into functions and build a great big library of those functions. > Use logically derived variable names (even if they're 5-10 characters). Naming your variables "a" wouldn't be accepted in any other languages, and from the outside looks like a pretty silly idea. >Phi shouldn't mean 30 things depending on the field you're in. Choose more descriptive variable names.
discreteevent 10y ago
He expressed something similar to what he had said in the forementioned talk, that conventional mathematical notation is unhelpful, and that we ought to be able to express things more clearly as programs. I agreed that I find conventional mathematical notation unhelpful; when I try to read papers there are concepts I easily understand as code but I can't parse the symbolic math of. "There's too much operator overloading", I said, "and that makes it hard for me to understand in which way a symbol is being used, and papers never seem to clarify." Sussman replied, "And it's not only the operator overloading! What's that 'x' doing there! That's why we put 'let' in Scheme!" https://dustycloud.org/blog/tag/sussman/ https://dustycloud.org/blog/tag/sussman/ Looks like you are not the only great mind to think of this (although I do also think that a diagram with some text can lead to the clearest explanations) There is a link to a video in that where Sussman explains the notation although there may be better ones also.
pcarbonn 10y ago
This reminds me of the effort by Sussman to teach physics by programming : Functional differential geometry [1] was discussed on hacker news before [2]. [1] https://mitpress.mit.edu/books/functional-differential-geometry https://mitpress.mit.edu/books/functional-differential-geome... [2] https://news.ycombinator.com/item?id=7884551 https://news.ycombinator.com/item?id=7884551
imakecomments 10y ago
You may be interested in Automated Theorem Proving: I quote the author Geoff Sutcliffe here: "Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement (the conjecture) is a logical consequence of a set of statements (the axioms and hypotheses). ATP systems are used in a wide variety of domains. For examples, a mathematician might prove the conjecture that groups of order two are commutative, from the axioms of group theory; a management consultant might formulate axioms that describe how organizations grow and interact, and from those axioms prove that organizational death rates decrease with age; a hardware developer might validate the design of a circuit by proving a conjecture that describes a circuit's performance, given axioms that describe the circuit itself; or a frustrated teenager might formulate the jumbled faces of a Rubik's cube as a conjecture and prove, from axioms that describe legal changes to the cube's configuration, that the cube can be rearranged to the solution state. All of these are tasks that can be performed by an ATP system, given an appropriate formulation of the problem as axioms, hypotheses, and a conjecture. The language in which the conjecture, hypotheses, and axioms (generically known as formulae) are written is a logic, often classical 1st order logic, but possibly a non-classical logic and possibly a higher order logic. These languages allow a precise formal statement of the necessary information, which can then be manipulated by an ATP system. This formality is the underlying strength of ATP: there is no ambiguity in the statement of the problem, as is often the case when using a natural language such as English. Users have to describe the problem at hand precisely and accurately, and this process in itself can lead to a clearer understanding of the problem domain. This in turn allows the user to formulate their problem appropriately for submission to an ATP system. The proofs produced by ATP systems describe how and why the conjecture follows from the axioms and hypotheses, in a manner that can be understood and agreed upon by everyone, even other computer programs. The proof output may not only be a convincing argument that the conjecture is a logical consequence of the axioms and hypotheses, it often also describes a process that may be implemented to solve some problem. For example, in the Rubik's cube example mentioned above, the proof would describe the sequence of moves that need to be made in order to solve the puzzle. ATP systems are enormously powerful computer programs, capable of solving immensely difficult problems. Because of this extreme capability, their application and operation sometimes needs to be guided by an expert in the domain of application, in order to solve problems in a reasonable amount of time. Thus ATP systems, despite the name, are often used by domain experts in an interactive way. The interaction may be at a very detailed level, where the user guides the inferences made by the system, or at a much higher level where the user determines intermediate lemmas to be proved on the way to the proof of a conjecture. There is often a synergetic relationship between ATP system users and the systems themselves: The system needs a precise description of the problem written in some logical form, the user is forced to think carefully about the problem in order to produce an appropriate formulation and hence acquires a deeper understanding of the problem, the system attempts to solve the problem, if successful the proof is a useful output, if unsuccessful the user can provide guidance, or try to prove some intermediate result, or examine the formulae to ensure that the problem is correctly described, and so the process iterates. ATP is thus a technology very suited to situations where a clear thinking domain expert can interact with a powerful tool, to solve interesting and deep problems. Potential ATP users need not be concerned that they need to write an ATP system themselves; there are many ATP systems readily available for use. At the 1st order level some well known and successful systems are Otter, E, SPASS, Vampire, and Waldmeister. Higher order systems include ACL2, Coq, HOL, and Nqthm. For examples of problems written in classical 1st order logic, the TPTP problem library is a useful resource, which also has a simple interface for users to try out many 1st order ATP systems. Fields where ATP has been successfully used include logic, mathematics, computer science, engineering, and social science; some outstanding successes are described below. There are potentially many more fields where ATP could be used, including biological sciences, medicine, commerce, etc. The technology is waiting for users from such fields." Link: http://www.cs.miami.edu/~tptp/OverviewOfATP.html http://www.cs.miami.edu/~tptp/OverviewOfATP.html
mathgenius 10y ago
> abstract, human-evaluatable, programming language? yes, it's happening: https://ncatlab.org/nlab/show/Globular https://ncatlab.org/nlab/show/Globular > Use logically derived variable names I agree. It just becomes a pain in the ass to write this stuff. The greek is math-asm for the hand. > completely standard way as to how to define all of your algorithms and logical assertions? people are working on it, for example: https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath "This coq library aims to formalize a substantial body of mathematics using the univalent point of view." One thing to note however is that the mathematics in the OP is inherently two (and higher) dimensional, and so it makes much more sense to adopt a language that is two (or higher) dimensional. Squashing it down into one dimensions (like with a usual language) creates a big mess.

doubleunplussed 10y ago

When you write a function, you still need to give the arguments names. When you write an algorithm and want to share it with someone, you still need to give the variables names. That's all the greek symbols are - and mathematical notation is an abstract, human evaluateable programming language. Common ideas are abstracted into functions, like sine, cosine - min, max, even weird things like Bessel functions, Legendre polynomials, these are all written as function(arguments) in maths. Maths has indexing, a bunch of operators, and what the operators do often depends on what type of objects they're applying to. Python's list and set comprehensions etc actually come from a real mathematical notation for defining sets. All those capital sigmas and capital pi's are reduction operators - sums and products. There isn't an assignment operator - you're expected to give each variable a unique name if you have a multi-stage process, so you only ever make statements of equality rather than assignment. Sure, it's an ambiguous language sometimes, but it sounds like your complaint comes down to standardising it more and using longer variable names.

gravypod 10y ago
> Sure, it's an ambiguous language sometimes, but it sounds like your complaint comes down to standardising it more and using longer variable names. Has unstandardization and shorter variable names ever been heralded as the icon of understandability? I think that answers how I feel about that. > When you write a function, you still need to give the arguments names. When you write an algorithm and want to share it with someone, you still need to give the variables names. That's all the greek symbols are - and mathematical notation is an abstract, human evaluateable programming language. I get that. When I write a loop over a space of integers I sometimes use "i" or "j". When I iterate over a 2d array I usually use "x" and "y" ("z" for 3d). If I'm writing networking/file code I usually have an array of N length of bytes called "buff" or "buffer". These are all common threads. But when I'm writing "buffer", "i", "j", "x", "y", or "z" they mean the same thing at every location in every piece of software to every software developer. But, and here's the big but, I get a tingling feeling every time I use one of these. I always ask myself "is this the meaning I'm attempting to convey"? If there's a slight variation I'll just rename the variable to a more verbose version to make it easier to follow. > Common ideas are abstracted into functions, like sine, cosine - min, max, even weird things like Bessel functions, Legendre polynomials, these are all written as function(arguments) in maths. I can't name an idea in computer science that isn't a function (in at least 1 major programming language). We can go so far as to say that the basic operators, right down to define, are functions in LISP. I can on the other hand name many ideas that aren't functions in "Math"-lang and I'm sure you can as well. > Python's list and set comprehensions etc actually come from a real mathematical notation for defining sets. The difference is python uses, for the most part, the ASCII character set and presents a simple-for-all notation. > All those capital sigmas and capital pi's are reduction operators - sums and products. Why does Pi and Sigma provide a better interface to these operations then apply and reduction notation of LISP? > There isn't an assignment operator - you're expected to give each variable a unique name if you have a multi-stage process, so you only ever make statements of equality rather than assignment. Am I just supposed to guess the starting state of a variable? How do I define variables based on others? What type is my new variable (collection, graph, tree, value)? Why not just have a simple variable name for every non-common variable (Pi for Pi or 3.14... is fine because it is a constant everywhere). Also, if there is a multi-stage process you should have multiple functions that define a subset of the solution, each with an appropriate name, each with appropriate "test-cases" (proofs) for that subset, each with documentation and type annotations to provide an understanding as to how it works. None of them should require domain-specific ideas to understand after you've read the "tests", docs, types, and names.

throwaway729 10y ago

> Am I wrong? Is this not possible? Yes, you're wrong. I mean, I agree with you. This is the route we should commit to. Building up mathematical theories in a programming language. But I think you've reached the right conclusion for horribly confused reasons, and that you severely over-estimate the state of the art in CS. This over-estimation results in you not realizing why something like this could be a valuable tool within the world you describe. Perhaps I'm wrong, but here's what gives me this impression: > Write human-provable "test-cases" Since the article is discussing mathematics, I suppose here by proof you actually really honestly mean proof. So proof by "I worked through 6 examples and they all turned out OK so far"? That's not typically what a mathematician means when they say they proved something. Proofs can get horribly complicated in ways that test cases generally don't. > Writing functions, "unit tests", building on abstractions, and creating "libraries" do help. We all know this because it works well in CS. Yes, all of these things would be great. But it's REALLY not that simple. Formal verification of software systems remains a mostly academic pursuit. There's some promising early work, but almost none of "us" formally verify our software. It does NOT work well in CS. Not at the moment. And most things we do in CS are conceptually simpler than a lot of mathematics. So exploring alternative interfaces makes a lot of sense. > Is this not possible? Is there a reason as to why math and logic can't be expressed as an abstract programing language? They can be. It's horrendously verbose, and it's difficult to do novel work in such a formal setting. It does not work well in the same sense that it does not work well in CS -- you can do it, if you're willing to spend 10x the time/money/effort for the "good enough" version (in math, paper proofs; in CS, shippable but unverified code).

gravypod 10y ago
> I think the problem is that you don't understand what a real result looks like in math Unfortunetly I've been plauged with the task of reading some math papers to understand some things in the past. I still wake up in a cold sweat some times. > So proof by "I worked through 6 examples and they all turned out OK so far"? > That's not typically what a mathematician means when they say they proved something... I'm well aware. That's why I included the quote marks. I mean a logical proof based on the relation of this "function's" suppositions in relation to the rest of the "functions" it is integrated with providing context and mathematical relations to the other parts of the conjecture you're working on. > Formal verification of software systems remains a mostly academic pursuit. There's some promising early work, but almost none of "us" formally verify our software. > So no, you're wrong. It does NOT work well in CS. Not at the moment. I mean this is just blatantly wrong and ignoring the face of what I'm saying. I'm implying that 1) if you have a pinical example of computer science you can take a freshman-level CS student, give them a tour of the language, and let them loose on a problem and they'll understand what's going on. Some of the worlds most complex simulation sytems have children in highschool writing games in them. Things like Unity and Unreal engine representing thousands and thousands of manhours to create along with entire libraries of research, industry-funded experiments, and years of expertise. I'm saying that the common practices of programming can yield systems that are simple for anyone to maintain and work on. I can't say the same for mathematics. While I understand the concepts of derivatives, integrals, and calculus if tasked I'd most likely not be able to provide a formula to define the area of a new shape despite understanding the core material far better then most programmers understand the new project they've been flung into. 2) the concepts from computer science and programming can be adapted to suit math's needs and these adaptations can be fluid where novel augmentations of the processes that yield positive results can be further integrated into mathematics. Programming and computer science are quickly evolving fields and have a unique possition in that many people engage in them without formal training from a university because in most cases it's simple unneeded. You can pick up one book and then rely on the common goal of every computer scientist and programmer that came before you: abstraction of the concepts to yield a simple solution to arbitrarily complex problems. Because of this you can jump anywhere and pick up and run with your work. I'm not saying these ideas are directly applicable with no modification. What I am saying is "these are the ideas that make my field possible" and suggesting that standardizing practices in the Math-heavy fields would not be a bad thing especially if these same standardized practices have been used to great lengths in our field to produce a set of very positive outcomes.

lend000 10y ago

The plethora of Greek symbols and italicized fonts for fancy operations make interesting research papers mostly unreadable for me. It would be great if mathematicians started using descriptive names for each variable (including non-obvious functions/operations), and weren't limited to one letter per symbol (i.e. I'm describing programming). Granted, there's too much momentum to change anything, especially since it would probably slow down the people doing the fancy math.

klodolph 10y ago
It's not just momentum. "Non-obvious" is relative. Every mathematical paper is built on top of thousands of pieces of foundational work, how do you pick which pieces of the foundation are obvious and which are non-obvious? And how do we even use descriptive names? Descriptive names were used in older works like Philosophiæ Naturalis Principia Mathematica which are practically unreadable (even when translated into your native language) compared to more modern ways of writing things like "F=ma", "F=mx''", or "F=m d^2x/dt^2", which are fantastic to understand. Or if I'm writing something like "x+0=x", is there really some descriptive name I can use for "x"? Or in short, we tried that and terse notation tends to be both easier to understand and more concise.

andrepd 10y ago

I have absolutely no idea what you're trying to say. What do you mean with all that? Maybe I'm being obtuse but you're just saying random words and terms from programming. How on earth is that applicable to physics? I have absolutely no idea what you're trying to propose.

gravypod 10y ago
The incorperation of broader programming principles and concepts that have evolved over the course of advancements in the creation of software systerms into other language-based fields including mathematics and standardization of these languages to lessen ambiguities. Things like using variable names that make sense rather then the current single-letter + subscript limit. Using easily typable characters and combining those to create complex operations. Substituting language for obtuse symbols. Simplification of expression syntax. I don't know best how to put it in your terms, nor what I'm missing, because these are things I take for granted being a programmer.
traverseda 10y ago
Well, not OP, but that was all very understandable to me, and resonated. I'll try to explain some specific points. >Why do this rather then define an abstract, human-evaluatable, programming language? The syntax of math is bad for a number of reasons. Making it some big 3D thing isn't going to make that syntax more reasonable. Math is a language that could learn a lot from programming languages, even if you don't plan on running it on a computer and dealing with all that hassle. >Making strange squigles on a page doesn't help. Making strange greek symbols on the page doesn't help. >Ditch the alphabet soup (and yes, even the 5th centry Greek alphabet soupe) Math is optimized for paper. This makes it a lot less accessible these days. All these custom glyphs are a damn weird idea. Naming your variables "a" wouldn't be accepted in any other languages. >Abstract common ideas into "functions". Once you've abandoned the idea of single-letter variable names, it becomes easier to abstract common mathematical ideas into functions and build a great big library of those functions. > Use logically derived variable names (even if they're 5-10 characters). Naming your variables "a" wouldn't be accepted in any other languages, and from the outside looks like a pretty silly idea. >Phi shouldn't mean 30 things depending on the field you're in. Choose more descriptive variable names.

discreteevent 10y ago

He expressed something similar to what he had said in the forementioned talk, that conventional mathematical notation is unhelpful, and that we ought to be able to express things more clearly as programs. I agreed that I find conventional mathematical notation unhelpful; when I try to read papers there are concepts I easily understand as code but I can't parse the symbolic math of. "There's too much operator overloading", I said, "and that makes it hard for me to understand in which way a symbol is being used, and papers never seem to clarify." Sussman replied, "And it's not only the operator overloading! What's that 'x' doing there! That's why we put 'let' in Scheme!" https://dustycloud.org/blog/tag/sussman/ https://dustycloud.org/blog/tag/sussman/ Looks like you are not the only great mind to think of this (although I do also think that a diagram with some text can lead to the clearest explanations) There is a link to a video in that where Sussman explains the notation although there may be better ones also.

pcarbonn 10y ago

This reminds me of the effort by Sussman to teach physics by programming : Functional differential geometry [1] was discussed on hacker news before [2]. [1] https://mitpress.mit.edu/books/functional-differential-geometry https://mitpress.mit.edu/books/functional-differential-geome... [2] https://news.ycombinator.com/item?id=7884551 https://news.ycombinator.com/item?id=7884551

imakecomments 10y ago

You may be interested in Automated Theorem Proving: I quote the author Geoff Sutcliffe here: "Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement (the conjecture) is a logical consequence of a set of statements (the axioms and hypotheses). ATP systems are used in a wide variety of domains. For examples, a mathematician might prove the conjecture that groups of order two are commutative, from the axioms of group theory; a management consultant might formulate axioms that describe how organizations grow and interact, and from those axioms prove that organizational death rates decrease with age; a hardware developer might validate the design of a circuit by proving a conjecture that describes a circuit's performance, given axioms that describe the circuit itself; or a frustrated teenager might formulate the jumbled faces of a Rubik's cube as a conjecture and prove, from axioms that describe legal changes to the cube's configuration, that the cube can be rearranged to the solution state. All of these are tasks that can be performed by an ATP system, given an appropriate formulation of the problem as axioms, hypotheses, and a conjecture. The language in which the conjecture, hypotheses, and axioms (generically known as formulae) are written is a logic, often classical 1st order logic, but possibly a non-classical logic and possibly a higher order logic. These languages allow a precise formal statement of the necessary information, which can then be manipulated by an ATP system. This formality is the underlying strength of ATP: there is no ambiguity in the statement of the problem, as is often the case when using a natural language such as English. Users have to describe the problem at hand precisely and accurately, and this process in itself can lead to a clearer understanding of the problem domain. This in turn allows the user to formulate their problem appropriately for submission to an ATP system. The proofs produced by ATP systems describe how and why the conjecture follows from the axioms and hypotheses, in a manner that can be understood and agreed upon by everyone, even other computer programs. The proof output may not only be a convincing argument that the conjecture is a logical consequence of the axioms and hypotheses, it often also describes a process that may be implemented to solve some problem. For example, in the Rubik's cube example mentioned above, the proof would describe the sequence of moves that need to be made in order to solve the puzzle. ATP systems are enormously powerful computer programs, capable of solving immensely difficult problems. Because of this extreme capability, their application and operation sometimes needs to be guided by an expert in the domain of application, in order to solve problems in a reasonable amount of time. Thus ATP systems, despite the name, are often used by domain experts in an interactive way. The interaction may be at a very detailed level, where the user guides the inferences made by the system, or at a much higher level where the user determines intermediate lemmas to be proved on the way to the proof of a conjecture. There is often a synergetic relationship between ATP system users and the systems themselves: The system needs a precise description of the problem written in some logical form, the user is forced to think carefully about the problem in order to produce an appropriate formulation and hence acquires a deeper understanding of the problem, the system attempts to solve the problem, if successful the proof is a useful output, if unsuccessful the user can provide guidance, or try to prove some intermediate result, or examine the formulae to ensure that the problem is correctly described, and so the process iterates. ATP is thus a technology very suited to situations where a clear thinking domain expert can interact with a powerful tool, to solve interesting and deep problems. Potential ATP users need not be concerned that they need to write an ATP system themselves; there are many ATP systems readily available for use. At the 1st order level some well known and successful systems are Otter, E, SPASS, Vampire, and Waldmeister. Higher order systems include ACL2, Coq, HOL, and Nqthm. For examples of problems written in classical 1st order logic, the TPTP problem library is a useful resource, which also has a simple interface for users to try out many 1st order ATP systems. Fields where ATP has been successfully used include logic, mathematics, computer science, engineering, and social science; some outstanding successes are described below. There are potentially many more fields where ATP could be used, including biological sciences, medicine, commerce, etc. The technology is waiting for users from such fields." Link: http://www.cs.miami.edu/~tptp/OverviewOfATP.html http://www.cs.miami.edu/~tptp/OverviewOfATP.html

mathgenius 10y ago

> abstract, human-evaluatable, programming language? yes, it's happening: https://ncatlab.org/nlab/show/Globular https://ncatlab.org/nlab/show/Globular > Use logically derived variable names I agree. It just becomes a pain in the ass to write this stuff. The greek is math-asm for the hand. > completely standard way as to how to define all of your algorithms and logical assertions? people are working on it, for example: https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath "This coq library aims to formalize a substantial body of mathematics using the univalent point of view." One thing to note however is that the mathematics in the OP is inherently two (and higher) dimensional, and so it makes much more sense to adopt a language that is two (or higher) dimensional. Squashing it down into one dimensions (like with a usual language) creates a big mess.