26 ms·

Math-as-Code (2015)

161 points by yinso 6y ago

truth_seeker 6y ago
Beautiful !
- angela112 6y ago
  yes beautiful !! <a href="http://167.172.68.72/"target="_blank">tokeqq</a> http://167.172.68.72/"target="_blank">tokeqq</a>
eterps 6y ago
I also liked how the Fortress programming language enabled you to switch between regular syntax and math notation: https://www.zdnet.com/article/guy-steeles-new-programming-language/ https://www.zdnet.com/article/guy-steeles-new-programming-la... The language has faded into obscurity though.
- eterps 6y ago
  There aren't many screenshots available, only a couple of lo-res images on Google image search: https://www.google.com/search?q="fortress" https://www.google.com/search?q="fortress" programming language mathematical&tbm=isch
- zorked 6y ago
  Mathematica has that, though the math notation is more about display than input.
  - henrikeh 6y ago
    Proper mathematical notation is absolutely for the input. Maybe not integrals and sums (which are a bit unclear), but fractions, powers and the more specialized notation is quite nice for readability.
BiteCode_dev 6y ago
I hear regularly completly opposite opinions: - the ones that wish programming would be more elegant and expressive like maths notations - the ones that wish paper would publish a Python algo instead because maths notations are inconsistant and hard to read I'm not a maths person, so can people with a lot of experience with it help me decide which one is the more reasonable?
- y7 6y ago
  Neither. Mathematical notation and programming languages serve two different purposes, and I think they both work pretty well for what they're designed to do. Math papers are about communicating with other humans, so they use the shortest language that is effective for the particular problem they're studying. Notation is not meant to be universally unambiguous, because that leads to a much larger language.
  - Koshkin 6y ago
    This difference must not be exaggerated. Mathematical notation is declarative/functional, and programming languages designed in a similar vein are not unheard of.
- yodelshady 6y ago
  No question about it. Mathematical notation is pure evil that should be cast into mount doom and then some. Mathematical notation makes Javascript operators look sane. There is barely a single operation in the last few maths papers I've read that doesn't have at least four possible interpretations at first glance, so the only way to understand a single line is to understand the entire theory at once. Needless to say, all variables are described with single letters. The best defense for it is that it evolved from handwriting, where the difference between `matmul(a,b)` and `a x b`, repeated a few dozen times, is significant. These days, as I type, I define commands to turn the unambiguous longhand into the shorthand. ("But yodel, a and b aren't bolded or uppercase so according to convention they must be scalars!", I hear you say. Ha, ha, ha.) I am genuinely angry about this. A great deal of practical mathematics is not hard. Mathematical notation is hard, and everyone using it should be a little bit ashamed at how needlessly difficult the field is.
ilaksh 6y ago
This is really cool, but where I get really lost in not on the more basic stuff covered here, but the more advanced math that shows up frequently in ML papers for example. It seems like there is a lot of stuff in math that is kind of like code libraries or functions in programming, except you are supposed to just remember exactly how it works rather than having the source code.
29athrowaway 6y ago
In JavaScript you should use Number.EPSILON rather than 1e-5
stared 6y ago
I've found that PyTorch is the smoothest for math <-> programming (at least when it comes to vector-like calculus). See for example gradient descent in maths (LaTeX) and in PyTorch: https://colab.research.google.com/github/stared/thinking-in-tensors-writing-in-pytorch/blob/master/2%20Gradient%20Descent.ipynb https://colab.research.google.com/github/stared/thinking-in-... For the smoothest math <-> programming
- dunefox 6y ago
  While I like PyTorch very much I have found Julia + Flux to be even better.
  - stared 6y ago
    Could you show some examples? I did try to use Julia quite a few times (including, I don't know 8 years ago), as I loved the philosophy (brief yet fast, types). Sadly, I never considered it readable - a mix of new concepts, legacy MATLAB syntax, and in general disregard for this part (even function names didn't have consistent naming). If it moved a lot with that respect, I would be happy some nice examples.
    - dunefox 6y ago
      I mean, that's a strange thing to say since PyTorch and especially Python are much further from the math than Julia and Flux. For example, if I want to regularise a layer: PyTorch: l2 = layer.pow(2).sum() loss += lambda * l2 Julia: l2 = sum(layer .^ 2) loss += λ * l2 I can just use regular Julia functions whereas in PyTorch I need to use special PyTorch functions as to not detach the tape. This only gets worse and less readable the more complex things I want to do.
      - stared 6y ago
        I guess one core thing is that I don't think that the traditional mathematical notation is particularly consistent. (For a reference, I published over a dozen mathematical papers.) I love when the "data-flow" is consistent, from left to right. The Julia code (and traditional mathematical notation) reads: middle, right, left. Plus, instead of inventing infix notation, I find it cleaner to write custom methods/functions rather than rely on (a fixed, limited, and non-apparent) set of built-in inflix operators. Made-up .^
Koshkin 6y ago
Mathematical notation is great at facilitating formal manipulations. This is its critical feature, and without it we would get stuck at the level of ancient mathematics. This is the reason it was invented a few hundred years ago in the first place. That said, I find that notation is often abused in texts as a mere substitute for the normal human language which, while allowing to compress the text, does in fact nothing to help the reader better understand what is being said but rather looks like a crazy mess of characters and other marks in a multitude of fonts, styles and sizes the only purpose of which seems to be to cause an eye strain.
- pfortuny 6y ago
  Exactly. Good maths does not use extensive “notation” per se, only when it is really necessary. Any good treatise has many more paragraphs of carefully written text than of equations: these are only used when they are truly required.
  - enriquto 6y ago
    Moreover, mathematical notation is very universally agreed upon. You can read a math paper in a language that you do not understand and just by looking at the formulas you can get quite a good idea of its contents, methods and proofs. For code, the situation is dire: each programming language has a particular, different, and often limited way to express math.
    - sohamsankaran 6y ago
      This is not even true across subfields in mathematics -- there's a lot of context-specific notational overloading, and there is often inconsistent notation even within a single long paper.
      - enriquto 6y ago
        Ok, but if you see something like ∫Ωf (with Ω as a subindex of ∫ ) you can be 100% sure that it means some kind of linear operator on an object "f", that is additive over disjoint union of the set parameter Ω, and a few other natural rules that are satisfied by integrals (monotony, positivity, etc). Of course in one paper it will mean Riemann integral, on another Lebesgue integral, an on another something completely different, defined axiomatically over discrete objects, but with exactly the same formal properties. In programming languages you have nothing universal like that, except maybe the notation for quoted strings. Such an integral may be written in some language as integration.integral.apply(omega, eff) on another as omega.getNaturalIntegrator().applyTo(eff) and yet on another as eff.integrateOver("planarDomain", omega) and on each of these constructions the visually evident formal properties of the integral are lost and difficult to reason about.
odc 6y ago
Oh. I was expecting someone to post the original APL paper here.
Schiphol 6y ago
I thought this was going to be about a math textbook (the ideas, not the notation) that relied on previous proficiency with code. [Category Theory for Programmers](https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...) meets this description. Is anyone familiar with any other good examples?
hntestacc 6y ago
This is a test. If you see this, please pass through.
sohamsankaran 6y ago
I would pay a fairly large chunk of my income to someone working on this kind of alternate representation of mathematics full-time. Email me at soham [at] soh.am if you're interested.
- zozbot234 6y ago
  The closest thing to this kind of alternate representation is formal mathematics, as seen in systems like Mizar, HOL Coq, Lean, Isabelle and the like. The fact that it generally "looks like computer code" is often seen as a drawback, but it does have its advantages. In fact, some of these systems allow for constructive theories, which means that they are programming languages of a sort.
  - sohamsankaran 6y ago
    I think there's a place for alternate representations like these outside of proofs that need to be exhaustively machine-checkable. I have, for what it's worth, had far better experiences with Coq and the like than with mathematics in general.
- elbear 6y ago
  I'm curious, what's your motivation for wanting this? I'm asking because: a) I'd be interested in your offer b) It's not clear how this alternate representation would look like. I'm hoping that your possible use cases would shed some light on that
xvilka 6y ago
In the future, I hope, there will be more convergence between formal proofs systems and the mathematical notation for learning, teaching, and storing knowledge. Systems like Lean, Coq, Sage Math, Octave, etc should work together on bringing more uniformity to the representation. Not for the actual code or an engine but some uniform language/format/interface, bringing the way to read and write it as a daily math, while preserving portability between those systems.
iamthemalto 6y ago
Am I missing something, or is the arrow operator (mathematical implication) not quite right in the example code they give? What happens when a statement is vacuously true?
augustt 6y ago
To be completely honest, I find it hard to believe when people claim that the reason they never 'got' mathematics was because of the notation. Actually understanding the concepts will almost always be significantly harder than understanding notation.
- doubleunplussed 6y ago
  There is a natural tendency to avoid learning the notation. Even though it would be easy, it goes against our instincts to intentionally go out of our way to look up notation we don't understand. With natural language one often picks up the meaning of new words based on context, after a bit of repetition. So it does not come naturally to people to do otherwise.
  - throwaway_pdp09 6y ago
    > to look up notation we don't understand Not so easy. I was trying to find out which of NN and ZZ was what, try searching for those. If you don't know what the signa (summing) sign means, how are you going to find it?
    - doubleunplussed 6y ago
      A quick google revealed this easily. Ctrl-f'ing this article https://en.wikipedia.org/wiki/List_of_mathematical_symbols https://en.wikipedia.org/wiki/List_of_mathematical_symbols for "Sigma" gets you that capital sigma is the summation symbol. ℤ etc are there too though they are admittedly harder to Ctrl-f for. Good luck googling for operators in a programming language as well though. Like with a programming language, for which you might want to skim a tutorial, if you are doing real analysis or whatever is talking about the sets of integers or natural numbers, you might want to skim the opening pages of a textbook or other course. The most common things are usually defined early on, and the less common things are often defined in-text when they are used, e.g "consider the bijective function f: ℤ→ℤ", now you know what f is and just need to google "bijective function". And if you do you'll see the notation about the domain and codomain (which you would also see in the opening chapters of an analysis textbook or lecture notes). I mean, learning how to use a programming language involves having to do some reading too to get to grips with hard-to-google things. Maths is no different.
analbumcover 6y ago
Homotopy type theory is a programming language whose original purpose was "math-as-code". Gaining widespread adoption among mathematicians, let alone programmers, seems unlikely as mathematicians dislike programming languages for their perceived lack of elegance and are firmly set in their set theoretic ways, while most programmers balk at the barest hint concision and rigor.
- rantwasp 6y ago
  programming is a special applied type of math.
- gergoerdi 6y ago
  HoTT isn't a programming language, because there are non-value normal forms. That's the whole reason behind research into various formulations of Cubical Type Theory, which is a programming language.
  - analbumcover 6y ago
    Intensional intuitionistic type theory is a programming language. Throw in higher inductive types (still a programming language at this point) and Voevodsky's univalence and you've got HoTT. Then sure, the simplicial model is not constructive, whereas the cubical models give computational meaning to univalence, but they're still just that, models of HoTT. So would you prefer I had said HoTT has models that are programming languages?
thelazydogsback 6y ago
I think the clear answer is that you want both -- maths notation, and at least one implementation in a non-specialized programming language with clear functional/procedural semantics. If you understand one or the other, you then you can also learn the mapping between the two. This is also important to remove ambiguities in notation, makes errors in each more obvious, and aids in reproducible results. Of course, applicable input and output data also needs to be supplied for verification. If the code is too long to publish in a paper (usually there is at least some core idea that can be expressed) then it should be in GitHub or elsewhere at a stable URI -- papers often refer to academic sites that 404 soon after. As a non-mathematician who has been recently been looking at papers in journal back-issues from about 1970 to 2010, I certainly would have benefited from this. On a related note, another issue is that that maths must be implicitly ordered in the context of the prose of the paper, while programs have actual entry-points and (without nitpicking) explicit ordering. (It's possible that ordering can be relaxed, but correctness preferred over runtime cost.) I think "maths-as-data" is more important here -- use a parsable common notation with enough meta-data that I can view it any way I want -- as math-with-greeks, math-with-friendly-names('en-us'), as APL, as plain Python, Python with numpy, etc.
gnramires 6y ago
If anyone is seriously interested in doing mathematics on the computer, give Sage a try. It gets rid of many machine-particularities, like floats not being real numbers (due to limited precision). You can easily represent and solve equations, do calculus, integration, etc. And it supports a python-like programming too. So you can write a for loop which solves an equation with different parameters at each iteration, for example. You can write logical proofs too, although that's not the main purpose. (I think doing calculations on your computer and generally being a superb Math assistant is where it's at).
- dependenttypes 6y ago
  > It gets rid of many machine-particularities, like floats not being real numbers (due to limited precision). I will have to doubt that for the simple fact that it is impossible to have a real number type on a computer.
  - gnramires 6y ago
    Real numbers are represented as abstract data structures, not as infinite series of digits (although that indeed fits in a Turing machine? :p) So for example, '2' is recognized as an integer and is represented using arbitrary size integers. You can also however write 'x = sqrt(2)' (or just 'sqrt(2)'), which has no finite digital (irrational), 'x' is a real number. You can then ask for finitely many digits of x, with 'x.n(5)' (gives 5 digits), or write something like 'y=x^3+3x-4', which gives another real number, represented as this polynomial data structure itself. The only problem with this is irreducibility. You can compose arbitrarily many operations on floats and still get a float of the same size. With this approach, it may not be possible to simplify a series of operations so the representation can grow unbounded. edit: Fun fact, there are (real) numbers that indeed cannot be represented in a finite computer no matter what -- but they cannot be represented in paper or uniquely represented in any finite abstract form either! This follows from the pigeonhole principle: finite expressions may represent numbers, but there are uncountably infinite (2^(N0)) real numbers, and only countably infinitely many expressions. So indeed almost every real cannot be represented. You can think of those as not being identifiable with any property, so there's no finite expression to describe them. They're more or less random.
rdlecler1 6y ago
I had a lot of trouble following mathematical (often analytical) notation because you could never drill down. It wasn’t until I started looking at the code making up math libraries that it all came together.
dang 6y ago
See also: 2017 (a bit): https://news.ycombinator.com/item?id=15948326 https://news.ycombinator.com/item?id=15948326 (another bit): https://news.ycombinator.com/item?id=15947744 https://news.ycombinator.com/item?id=15947744 2015: https://news.ycombinator.com/item?id=9805071 https://news.ycombinator.com/item?id=9805071 2015 (a bit): https://news.ycombinator.com/item?id=9801620 https://news.ycombinator.com/item?id=9801620
percentcer 6y ago
Weird that they left out the completely baffling yet for some reason ubiquitous Leibniz notation
vthommeret 6y ago
I plan to create a Show HN shortly, but I created an interactive Python tutorial to teach engineers how to read and implement math using the NumPy library, called Math to Code: https://mathtocode.com https://mathtocode.com It takes you from basic functions like square roots and absolute values, to summations, matrix multiplication, to measures like standard deviation and the Frobenius norm. I was inspired to create it while taking the Fast.ai course and Jeremy Howard showing what looked like a "complicated" Frobenius norm equation that could be implemented in a single line of Python. It's open source and should also work on mobile.
_hardwaregeek 6y ago
I highly recommend reading The Little Typer if you want a great book that bridges math and code. It starts out describing Pi, a Lisp with some interesting restrictions (limited recursion, types can have values, etc.). They build up some cool stuff like vectors with the size encoded in the type. All of a sudden, they explain that equality is a type, and any value of said type is a proof! Turns out you can think of many proofs as manipulating data structures to get a value of a certain type. I wonder how long until we get a somewhat mainstream language with pi types. I know Rust considered adding them. And I recently learned that Rust does allow for quantification over lifetimes^[1]. I could certainly see a language that implements dependently typed arrays. Midori for instance looked into eliding bounds checks with compiler proofs^[2]. [1]: https://doc.rust-lang.org/beta/nomicon/hrtb.html https://doc.rust-lang.org/beta/nomicon/hrtb.html [2]: http://joeduffyblog.com/2016/02/07/the-error-model/ http://joeduffyblog.com/2016/02/07/the-error-model/
- somethingsome 6y ago
  You should take a look into Lean Theorem Prover (among others) ;)
- gergoerdi 6y ago
  I think at this point, Haskell is the most likely to become the first mainstream PL with Pi types: https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell
winrid 6y ago
I love this kind of stuff. Following this thread for books. Currently I'm doing Data Science From Scratch except in C++ instead of Python. https://github.com/winrid/data-science-from-scratch-cpp https://github.com/winrid/data-science-from-scratch-cpp

Math-as-Code (2015)

161 points by yinso 6y ago

truth_seeker 6y ago

Beautiful !

angela112 6y ago
yes beautiful !! <a href="http://167.172.68.72/"target="_blank">tokeqq</a> http://167.172.68.72/"target="_blank">tokeqq</a>

eterps 6y ago

I also liked how the Fortress programming language enabled you to switch between regular syntax and math notation: https://www.zdnet.com/article/guy-steeles-new-programming-language/ https://www.zdnet.com/article/guy-steeles-new-programming-la... The language has faded into obscurity though.

eterps 6y ago
There aren't many screenshots available, only a couple of lo-res images on Google image search: https://www.google.com/search?q="fortress" https://www.google.com/search?q="fortress" programming language mathematical&tbm=isch
zorked 6y ago
Mathematica has that, though the math notation is more about display than input.
- henrikeh 6y ago
  Proper mathematical notation is absolutely for the input. Maybe not integrals and sums (which are a bit unclear), but fractions, powers and the more specialized notation is quite nice for readability.

BiteCode_dev 6y ago

I hear regularly completly opposite opinions: - the ones that wish programming would be more elegant and expressive like maths notations - the ones that wish paper would publish a Python algo instead because maths notations are inconsistant and hard to read I'm not a maths person, so can people with a lot of experience with it help me decide which one is the more reasonable?

y7 6y ago
Neither. Mathematical notation and programming languages serve two different purposes, and I think they both work pretty well for what they're designed to do. Math papers are about communicating with other humans, so they use the shortest language that is effective for the particular problem they're studying. Notation is not meant to be universally unambiguous, because that leads to a much larger language.
- Koshkin 6y ago
  This difference must not be exaggerated. Mathematical notation is declarative/functional, and programming languages designed in a similar vein are not unheard of.
yodelshady 6y ago
No question about it. Mathematical notation is pure evil that should be cast into mount doom and then some. Mathematical notation makes Javascript operators look sane. There is barely a single operation in the last few maths papers I've read that doesn't have at least four possible interpretations at first glance, so the only way to understand a single line is to understand the entire theory at once. Needless to say, all variables are described with single letters. The best defense for it is that it evolved from handwriting, where the difference between `matmul(a,b)` and `a x b`, repeated a few dozen times, is significant. These days, as I type, I define commands to turn the unambiguous longhand into the shorthand. ("But yodel, a and b aren't bolded or uppercase so according to convention they must be scalars!", I hear you say. Ha, ha, ha.) I am genuinely angry about this. A great deal of practical mathematics is not hard. Mathematical notation is hard, and everyone using it should be a little bit ashamed at how needlessly difficult the field is.

ilaksh 6y ago

This is really cool, but where I get really lost in not on the more basic stuff covered here, but the more advanced math that shows up frequently in ML papers for example. It seems like there is a lot of stuff in math that is kind of like code libraries or functions in programming, except you are supposed to just remember exactly how it works rather than having the source code.

29athrowaway 6y ago

In JavaScript you should use Number.EPSILON rather than 1e-5

stared 6y ago

I've found that PyTorch is the smoothest for math <-> programming (at least when it comes to vector-like calculus). See for example gradient descent in maths (LaTeX) and in PyTorch: https://colab.research.google.com/github/stared/thinking-in-tensors-writing-in-pytorch/blob/master/2%20Gradient%20Descent.ipynb https://colab.research.google.com/github/stared/thinking-in-... For the smoothest math <-> programming

dunefox 6y ago
While I like PyTorch very much I have found Julia + Flux to be even better.
- stared 6y ago
  Could you show some examples? I did try to use Julia quite a few times (including, I don't know 8 years ago), as I loved the philosophy (brief yet fast, types). Sadly, I never considered it readable - a mix of new concepts, legacy MATLAB syntax, and in general disregard for this part (even function names didn't have consistent naming). If it moved a lot with that respect, I would be happy some nice examples.
  - dunefox 6y ago
    I mean, that's a strange thing to say since PyTorch and especially Python are much further from the math than Julia and Flux. For example, if I want to regularise a layer: PyTorch: l2 = layer.pow(2).sum() loss += lambda * l2 Julia: l2 = sum(layer .^ 2) loss += λ * l2 I can just use regular Julia functions whereas in PyTorch I need to use special PyTorch functions as to not detach the tape. This only gets worse and less readable the more complex things I want to do.
    - stared 6y ago
      I guess one core thing is that I don't think that the traditional mathematical notation is particularly consistent. (For a reference, I published over a dozen mathematical papers.) I love when the "data-flow" is consistent, from left to right. The Julia code (and traditional mathematical notation) reads: middle, right, left. Plus, instead of inventing infix notation, I find it cleaner to write custom methods/functions rather than rely on (a fixed, limited, and non-apparent) set of built-in inflix operators. Made-up .^

Koshkin 6y ago

Mathematical notation is great at facilitating formal manipulations. This is its critical feature, and without it we would get stuck at the level of ancient mathematics. This is the reason it was invented a few hundred years ago in the first place. That said, I find that notation is often abused in texts as a mere substitute for the normal human language which, while allowing to compress the text, does in fact nothing to help the reader better understand what is being said but rather looks like a crazy mess of characters and other marks in a multitude of fonts, styles and sizes the only purpose of which seems to be to cause an eye strain.

pfortuny 6y ago
Exactly. Good maths does not use extensive “notation” per se, only when it is really necessary. Any good treatise has many more paragraphs of carefully written text than of equations: these are only used when they are truly required.
- enriquto 6y ago
  Moreover, mathematical notation is very universally agreed upon. You can read a math paper in a language that you do not understand and just by looking at the formulas you can get quite a good idea of its contents, methods and proofs. For code, the situation is dire: each programming language has a particular, different, and often limited way to express math.
  - sohamsankaran 6y ago
    This is not even true across subfields in mathematics -- there's a lot of context-specific notational overloading, and there is often inconsistent notation even within a single long paper.
    - enriquto 6y ago
      Ok, but if you see something like ∫Ωf (with Ω as a subindex of ∫ ) you can be 100% sure that it means some kind of linear operator on an object "f", that is additive over disjoint union of the set parameter Ω, and a few other natural rules that are satisfied by integrals (monotony, positivity, etc). Of course in one paper it will mean Riemann integral, on another Lebesgue integral, an on another something completely different, defined axiomatically over discrete objects, but with exactly the same formal properties. In programming languages you have nothing universal like that, except maybe the notation for quoted strings. Such an integral may be written in some language as integration.integral.apply(omega, eff) on another as omega.getNaturalIntegrator().applyTo(eff) and yet on another as eff.integrateOver("planarDomain", omega) and on each of these constructions the visually evident formal properties of the integral are lost and difficult to reason about.

odc 6y ago

Oh. I was expecting someone to post the original APL paper here.

Schiphol 6y ago

I thought this was going to be about a math textbook (the ideas, not the notation) that relied on previous proficiency with code. [Category Theory for Programmers](https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...) meets this description. Is anyone familiar with any other good examples?

hntestacc 6y ago

This is a test. If you see this, please pass through.

sohamsankaran 6y ago

I would pay a fairly large chunk of my income to someone working on this kind of alternate representation of mathematics full-time. Email me at soham [at] soh.am if you're interested.

zozbot234 6y ago
The closest thing to this kind of alternate representation is formal mathematics, as seen in systems like Mizar, HOL Coq, Lean, Isabelle and the like. The fact that it generally "looks like computer code" is often seen as a drawback, but it does have its advantages. In fact, some of these systems allow for constructive theories, which means that they are programming languages of a sort.
- sohamsankaran 6y ago
  I think there's a place for alternate representations like these outside of proofs that need to be exhaustively machine-checkable. I have, for what it's worth, had far better experiences with Coq and the like than with mathematics in general.
elbear 6y ago
I'm curious, what's your motivation for wanting this? I'm asking because: a) I'd be interested in your offer b) It's not clear how this alternate representation would look like. I'm hoping that your possible use cases would shed some light on that

xvilka 6y ago

In the future, I hope, there will be more convergence between formal proofs systems and the mathematical notation for learning, teaching, and storing knowledge. Systems like Lean, Coq, Sage Math, Octave, etc should work together on bringing more uniformity to the representation. Not for the actual code or an engine but some uniform language/format/interface, bringing the way to read and write it as a daily math, while preserving portability between those systems.

iamthemalto 6y ago

Am I missing something, or is the arrow operator (mathematical implication) not quite right in the example code they give? What happens when a statement is vacuously true?

augustt 6y ago

To be completely honest, I find it hard to believe when people claim that the reason they never 'got' mathematics was because of the notation. Actually understanding the concepts will almost always be significantly harder than understanding notation.

doubleunplussed 6y ago
There is a natural tendency to avoid learning the notation. Even though it would be easy, it goes against our instincts to intentionally go out of our way to look up notation we don't understand. With natural language one often picks up the meaning of new words based on context, after a bit of repetition. So it does not come naturally to people to do otherwise.
- throwaway_pdp09 6y ago
  > to look up notation we don't understand Not so easy. I was trying to find out which of NN and ZZ was what, try searching for those. If you don't know what the signa (summing) sign means, how are you going to find it?
  - doubleunplussed 6y ago
    A quick google revealed this easily. Ctrl-f'ing this article https://en.wikipedia.org/wiki/List_of_mathematical_symbols https://en.wikipedia.org/wiki/List_of_mathematical_symbols for "Sigma" gets you that capital sigma is the summation symbol. ℤ etc are there too though they are admittedly harder to Ctrl-f for. Good luck googling for operators in a programming language as well though. Like with a programming language, for which you might want to skim a tutorial, if you are doing real analysis or whatever is talking about the sets of integers or natural numbers, you might want to skim the opening pages of a textbook or other course. The most common things are usually defined early on, and the less common things are often defined in-text when they are used, e.g "consider the bijective function f: ℤ→ℤ", now you know what f is and just need to google "bijective function". And if you do you'll see the notation about the domain and codomain (which you would also see in the opening chapters of an analysis textbook or lecture notes). I mean, learning how to use a programming language involves having to do some reading too to get to grips with hard-to-google things. Maths is no different.

analbumcover 6y ago

Homotopy type theory is a programming language whose original purpose was "math-as-code". Gaining widespread adoption among mathematicians, let alone programmers, seems unlikely as mathematicians dislike programming languages for their perceived lack of elegance and are firmly set in their set theoretic ways, while most programmers balk at the barest hint concision and rigor.

rantwasp 6y ago
programming is a special applied type of math.
gergoerdi 6y ago
HoTT isn't a programming language, because there are non-value normal forms. That's the whole reason behind research into various formulations of Cubical Type Theory, which is a programming language.
- analbumcover 6y ago
  Intensional intuitionistic type theory is a programming language. Throw in higher inductive types (still a programming language at this point) and Voevodsky's univalence and you've got HoTT. Then sure, the simplicial model is not constructive, whereas the cubical models give computational meaning to univalence, but they're still just that, models of HoTT. So would you prefer I had said HoTT has models that are programming languages?

thelazydogsback 6y ago

I think the clear answer is that you want both -- maths notation, and at least one implementation in a non-specialized programming language with clear functional/procedural semantics. If you understand one or the other, you then you can also learn the mapping between the two. This is also important to remove ambiguities in notation, makes errors in each more obvious, and aids in reproducible results. Of course, applicable input and output data also needs to be supplied for verification. If the code is too long to publish in a paper (usually there is at least some core idea that can be expressed) then it should be in GitHub or elsewhere at a stable URI -- papers often refer to academic sites that 404 soon after. As a non-mathematician who has been recently been looking at papers in journal back-issues from about 1970 to 2010, I certainly would have benefited from this. On a related note, another issue is that that maths must be implicitly ordered in the context of the prose of the paper, while programs have actual entry-points and (without nitpicking) explicit ordering. (It's possible that ordering can be relaxed, but correctness preferred over runtime cost.) I think "maths-as-data" is more important here -- use a parsable common notation with enough meta-data that I can view it any way I want -- as math-with-greeks, math-with-friendly-names('en-us'), as APL, as plain Python, Python with numpy, etc.

gnramires 6y ago

If anyone is seriously interested in doing mathematics on the computer, give Sage a try. It gets rid of many machine-particularities, like floats not being real numbers (due to limited precision). You can easily represent and solve equations, do calculus, integration, etc. And it supports a python-like programming too. So you can write a for loop which solves an equation with different parameters at each iteration, for example. You can write logical proofs too, although that's not the main purpose. (I think doing calculations on your computer and generally being a superb Math assistant is where it's at).

dependenttypes 6y ago
> It gets rid of many machine-particularities, like floats not being real numbers (due to limited precision). I will have to doubt that for the simple fact that it is impossible to have a real number type on a computer.
- gnramires 6y ago
  Real numbers are represented as abstract data structures, not as infinite series of digits (although that indeed fits in a Turing machine? :p) So for example, '2' is recognized as an integer and is represented using arbitrary size integers. You can also however write 'x = sqrt(2)' (or just 'sqrt(2)'), which has no finite digital (irrational), 'x' is a real number. You can then ask for finitely many digits of x, with 'x.n(5)' (gives 5 digits), or write something like 'y=x^3+3x-4', which gives another real number, represented as this polynomial data structure itself. The only problem with this is irreducibility. You can compose arbitrarily many operations on floats and still get a float of the same size. With this approach, it may not be possible to simplify a series of operations so the representation can grow unbounded. edit: Fun fact, there are (real) numbers that indeed cannot be represented in a finite computer no matter what -- but they cannot be represented in paper or uniquely represented in any finite abstract form either! This follows from the pigeonhole principle: finite expressions may represent numbers, but there are uncountably infinite (2^(N0)) real numbers, and only countably infinitely many expressions. So indeed almost every real cannot be represented. You can think of those as not being identifiable with any property, so there's no finite expression to describe them. They're more or less random.

rdlecler1 6y ago

I had a lot of trouble following mathematical (often analytical) notation because you could never drill down. It wasn’t until I started looking at the code making up math libraries that it all came together.

dang 6y ago

See also: 2017 (a bit): https://news.ycombinator.com/item?id=15948326 https://news.ycombinator.com/item?id=15948326 (another bit): https://news.ycombinator.com/item?id=15947744 https://news.ycombinator.com/item?id=15947744 2015: https://news.ycombinator.com/item?id=9805071 https://news.ycombinator.com/item?id=9805071 2015 (a bit): https://news.ycombinator.com/item?id=9801620 https://news.ycombinator.com/item?id=9801620

percentcer 6y ago

Weird that they left out the completely baffling yet for some reason ubiquitous Leibniz notation

vthommeret 6y ago

I plan to create a Show HN shortly, but I created an interactive Python tutorial to teach engineers how to read and implement math using the NumPy library, called Math to Code: https://mathtocode.com https://mathtocode.com It takes you from basic functions like square roots and absolute values, to summations, matrix multiplication, to measures like standard deviation and the Frobenius norm. I was inspired to create it while taking the Fast.ai course and Jeremy Howard showing what looked like a "complicated" Frobenius norm equation that could be implemented in a single line of Python. It's open source and should also work on mobile.

_hardwaregeek 6y ago

I highly recommend reading The Little Typer if you want a great book that bridges math and code. It starts out describing Pi, a Lisp with some interesting restrictions (limited recursion, types can have values, etc.). They build up some cool stuff like vectors with the size encoded in the type. All of a sudden, they explain that equality is a type, and any value of said type is a proof! Turns out you can think of many proofs as manipulating data structures to get a value of a certain type. I wonder how long until we get a somewhat mainstream language with pi types. I know Rust considered adding them. And I recently learned that Rust does allow for quantification over lifetimes^[1]. I could certainly see a language that implements dependently typed arrays. Midori for instance looked into eliding bounds checks with compiler proofs^[2]. [1]: https://doc.rust-lang.org/beta/nomicon/hrtb.html https://doc.rust-lang.org/beta/nomicon/hrtb.html [2]: http://joeduffyblog.com/2016/02/07/the-error-model/ http://joeduffyblog.com/2016/02/07/the-error-model/

somethingsome 6y ago
You should take a look into Lean Theorem Prover (among others) ;)
gergoerdi 6y ago
I think at this point, Haskell is the most likely to become the first mainstream PL with Pi types: https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell

winrid 6y ago

I love this kind of stuff. Following this thread for books. Currently I'm doing Data Science From Scratch except in C++ instead of Python. https://github.com/winrid/data-science-from-scratch-cpp https://github.com/winrid/data-science-from-scratch-cpp