4 ms·

How to Write Software with Mathematical Perfection

51 points by theafh 4y ago

hintymad 4y ago
In theory both programming and mathematics command rigorous and abstract thinking, yet somehow millions of software engineers, or so I guess, find even college-level maths hard. My theory is that programming has much less leaky abstractions than math. If I used PyTorch, for instance, I don't really need to understand how chain rule works or how matrix derivatives work for most cases. If I use Netty or NIO in Java , I don't really need to have in-depth understanding of OS, TCP/IP, or any of the algorithms covered in books like The Art of Multiprocessor Programming. In contrast, maths "leak" its abstraction left and right from top to bottom. Let's say I want to learn and use PCA, a quite straightforward concept in entry-level linear algebra, I would have to understand vector, matrix, vector space, coordinate system, eigenvalue, covariance, orthogonality, and etc. Each concept recursively requires more layers to understand, and combining the concepts require other math tools as well.
raxxorraxor 4y ago
I believe he is correct. As a more unqualified opinion from someone who codes (not necessarily programs) a lot of spin loops for embedded systems, I am also convinced that software devs should also become drummers. Perhaps not really but the sound would be awesome. I believe TLA+ is the better and more precise description of state machines and would very much reduce the verbosity for complex systems. From there the abstraction for new languages should happen. Here are some examples for that from Lamport himself: https://lamport.azurewebsites.net/video/video2-script.pdf https://lamport.azurewebsites.net/video/video2-script.pdf
- solarmist 4y ago
  This is interesting. Why drummers? I know programmers are drawn to music and languages as other interests, but you seem to have something specific in mind.
  - walleeee 4y ago
    Speaking as one, a drummer must have something called limb independence, which means the right leg might be playing one pattern on the kick drum, left leg a different pattern on the hihat (or a double pedal etc), who knows what's going on in the hands, and yet it all has to come together and sound synchronized. This doesn't seem so different, conceptually, from managing mental models of several independent processes doing various things on various schedules, while making sure the whole distributed program acts coherently to produce the expected output. Just a theory! I don't know how much the two faculties really overlap.
  - raxxorraxor 4y ago
    The drummer part wasn't meant that seriously. Just that a spin loop of an embedded system that controls a machine has a certain rhythm to it with very precise timings. Perhaps I am just under the illusion that my programs are some form of ballad. Thinking more on it I would be quite afraid if my µC starts any kind of solo.
webmaven 4y ago
The headline and lede on the page are a bit better: > How to Write Software With Mathematical Perfection > Leslie Lamport revolutionized how computers talk to each other. Now he’s working on how engineers talk to their machines.

51 points by theafh 4y ago

In theory both programming and mathematics command rigorous and abstract thinking, yet somehow millions of software engineers, or so I guess, find even college-level maths hard. My theory is that programming has much less leaky abstractions than math. If I used PyTorch, for instance, I don't really need to understand how chain rule works or how matrix derivatives work for most cases. If I use Netty or NIO in Java , I don't really need to have in-depth understanding of OS, TCP/IP, or any of the algorithms covered in books like The Art of Multiprocessor Programming. In contrast, maths "leak" its abstraction left and right from top to bottom. Let's say I want to learn and use PCA, a quite straightforward concept in entry-level linear algebra, I would have to understand vector, matrix, vector space, coordinate system, eigenvalue, covariance, orthogonality, and etc. Each concept recursively requires more layers to understand, and combining the concepts require other math tools as well.

raxxorraxor 4y ago

I believe he is correct. As a more unqualified opinion from someone who codes (not necessarily programs) a lot of spin loops for embedded systems, I am also convinced that software devs should also become drummers. Perhaps not really but the sound would be awesome. I believe TLA+ is the better and more precise description of state machines and would very much reduce the verbosity for complex systems. From there the abstraction for new languages should happen. Here are some examples for that from Lamport himself: https://lamport.azurewebsites.net/video/video2-script.pdf https://lamport.azurewebsites.net/video/video2-script.pdf

solarmist 4y ago
This is interesting. Why drummers? I know programmers are drawn to music and languages as other interests, but you seem to have something specific in mind.
- walleeee 4y ago
  Speaking as one, a drummer must have something called limb independence, which means the right leg might be playing one pattern on the kick drum, left leg a different pattern on the hihat (or a double pedal etc), who knows what's going on in the hands, and yet it all has to come together and sound synchronized. This doesn't seem so different, conceptually, from managing mental models of several independent processes doing various things on various schedules, while making sure the whole distributed program acts coherently to produce the expected output. Just a theory! I don't know how much the two faculties really overlap.
- raxxorraxor 4y ago
  The drummer part wasn't meant that seriously. Just that a spin loop of an embedded system that controls a machine has a certain rhythm to it with very precise timings. Perhaps I am just under the illusion that my programs are some form of ballad. Thinking more on it I would be quite afraid if my µC starts any kind of solo.

webmaven 4y ago

The headline and lede on the page are a bit better: > How to Write Software With Mathematical Perfection > Leslie Lamport revolutionized how computers talk to each other. Now he’s working on how engineers talk to their machines.