Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Think in Math, Write in Code

justinmeiners.github.io

Post reply on HN
Print view View original

171–180 of 256 posts

Re: Think in Math, Write in Code

#171

Post by dkarl »

misterdoubt wrote: post #136
dkarl wrote: post #133

Earlier quoted context omitted.

Math has more aspects than just logical deduction via mechanical rules. Math also has an aesthetic aspect that guides people to find elegant, powerful solutions within the space defined by the mechanical rules. There may be many paths of deduction from point A to point B, which are all mechanically equally valid. But from the human point of view, they have different value. Some will be simple and easy to understand;…

Ah, well, you just described the relative value of math in much the way I'd describe the relative value of... well, just about any intellectual pursuit. Same in philosophy. Or in law. Or in physics. A lot of people with particular interest in one area -- say, mathematics -- don't realize that much of what is important is much more generally applicable. It's not that these things are distinctly important for math. It'…

That's true to a certain extent, but math and programming share the property of being built up from logical building blocks that are combined in strict logical ways. Law and philosophy are built on language and culture; physics is closer but is empirical. Math and programs are built from logic, and this gives them more of a common aesthetic sense.

For example, in law or philosophy, repeating the same argument multiple times, adapted for different circumstances, can give it weight. In math and programming, the weight of repetition is dead weight that people strive to eliminate. In law and philosophy, arguments are built out of words and shared assumptions that change over time; in math, new definitions can be added, and terms can be confusingly overloaded, but old definitions remain accessible in a way that old cultural assumptions are not accessible to someone writing a legal argument.

In physics, the real world is a given, and we approximate it as best we can. In math and software, reality is chosen from the systems we are able to construct. Think of all the things in our society that would be different if they were not constrained by our ability to construct software. Traffic, for one — there would be no human drivers and almost zero traffic deaths.

Where programming differs from math is that math is limited only by human constraints. Running programs on real hardware imposes additional constraints that interact with the human ones.

Re: Think in Math, Write in Code

#172

Post by pron »

hwayne wrote: post #169
pron wrote: post #126

Earlier quoted context omitted.

I prefer TLA+ (it's both simpler and more powerful than PlusCal), except when specifying something at the code level (e.g. something like weak-memory-model concurrency algorithm).

For 95% of people, PlusCal will suit them just fine. I'm starting to see people say "I shouldn't learn PlusCal because it's not really TLA+", get disheartened about how difficult TLA+ is to learn, and believe they aren't able to use formal methods. I'd rather 10 people use a slightly-more-limited tool than 1 person use "the real thing".

I don't think TLA+ is "the real thing." I just find it easier. If others find PlusCal easier, then they should definitely start with that.

Re: Think in Math, Write in Code

#173

Post by nwallin »

0x445442 wrote: post #94
rowanG077 wrote: post #78

Earlier quoted context omitted.

Building software is not even remotely the same thing as building a bridge. It would be more akin to the architect creating the drawings twice for the bridge. Once as an exploratory version and the second one the production version. Oh wait that is actually how architects work. In fact at my work we have multiple CAD designers(not architects though) and it's not uncommon for them to completely throw away a design and…

I'll bet the engineering process of the software written for the Apollo 11 lunar lander was much closer to the bridge building process than you might think. I'll also bet there's a whole host of software projects which use similar processes today. It's just that most of us writing DB skins for "The Enterprise" are rarely, if ever exposed to real engineering for the simple fact that quality software is expensive and t…

> I'll bet the engineering process of the software written for the Apollo 11 lunar lander was much closer to the bridge building process than you might think.

Of course, but the Apollo 11 lunar lander was created without the aid of ubiquitous desktop computers. I imagine the SpaceX guidance/control software was written in a way that less resembles bridge-building/Apollo 11 lunar landers and more like the organic processes we see elsewhere in the software industry.

If Neo were to build a bridge in the Matrix, chances are his processes would bear little resemblance to those of the Army Corp of Engineers.

Re: Think in Math, Write in Code

#174

Post by agentultra »

svieira wrote: post #64
pron wrote: post #35

As the author notes, Leslie Lamport makes much of the same point, but more rigorously. You can find it in many of his writings, e.g. http://lamport.azurewebsites.net/pubs/state-machine.pdf Lamport's TLA+ makes this formal. It is a language based on simple mathematics + some temporal logic for reasoning about discrete systems (software, hardware) as well as hybrid discrete-continuous systems, and is increasingly used…

> and then show that a particular sorting program is indeed an implementation of Quicksort. I wasn't aware that TLA+ made this part possible. How do you map from TLA+ to C++ (for example) with certainty?

Refinement calculus is what it's formally referred to as. As pr0n has mentioned you start with a high-level, abstract model. You then create a second model that implies every invariant of the first while adding more detail. You proceed like this to get closer to the implementation. If you are satisfied they are one and the same you can stop.

However the goal isn't often to verify every single line of code. That would be prohibitively time consuming and expensive. The ideal use for this stuff is to verify the hard parts that are critical to get right. Verifying that a critical section of code will not lead to a deadlock or resource contention might be really important and so you could start with verifying that particular system.

Re: Think in Math, Write in Code

#175

Post by justinmeiners »

geomark wrote: post #71
warent wrote: post #8

There's an unpopular and somewhat seemingly contradictory opinion that I have regarding this, because this isn't the first time I've seen this topic brought up. Mathematics and programming are not really all that related to each other and I think there's an overemphasis on the importance of math in programming for 99% of applications. Sure, mathematical thinking can be useful, but it's only one type of logical thinki…

I've been thinking about this quite a bit, but coming from a different angle. I've been helping at my kid's school with coding clubs for primary students. When teachers are recruiting for the coding club they always mention the students who are good at math as good candidates. But what I have noticed is that the students who do the best in coding are more often musically inclined or linguistically talented. It seems…

You may be surprised that this also applies to math.

High-level math values logical and linguistic skills. This is often a hard stopping point for many students who were good at high school computation like calculus.

Re: Think in Math, Write in Code

#176

Post by justinmeiners »

geomark wrote: post #112
Junk_Collector wrote: post #82

Earlier quoted context omitted.

It's also worth thinking about that you don't really learn math in primary school so much as you learn numbers and computation, so when a teacher says a child is good at math they usually mean good at numbers. Very few teachers understand math well enough to identify who would be good at it and a lot of unfortunate students find this out when they get to college.

Sure, I can see that. But isn't it similar with language and other subjects? You just learn the basics, nothing deep, no turns of phrases, little expressiveness. Perhaps there is little correlation between those who excel at coding at a young age and those who go on to be good programmers when they get older. I just find it interesting that at this young age I see a correlation between coding skills and language skil…

Math is somewhat unique in that the high-school and early college version is not at all representative of the real thing. Its not "just a taste", its qualitatively different.

As the other comment above mentioned, I think this has to do with education of the teachers. Very few teachers know what math is either.

Re: Think in Math, Write in Code

#177

Post by seanmcdirmid »

j88439h84 wrote: post #166
seanmcdirmid wrote: post #138

Earlier quoted context omitted.

Math can be considered an art, though not a fine art. Programming by either extension is an art (though again, not a fine art). https://en.m.wikipedia.org/wiki/Mathematics_and_art

I don't see why it couldn't be a fine art.

Perhaps it could be practiced as part of a fine art, but like carpentry, programming itself isn’t.

Re: Think in Math, Write in Code

#178

Post by crimsonalucard »

warent wrote: post #8

There's an unpopular and somewhat seemingly contradictory opinion that I have regarding this, because this isn't the first time I've seen this topic brought up. Mathematics and programming are not really all that related to each other and I think there's an overemphasis on the importance of math in programming for 99% of applications. Sure, mathematical thinking can be useful, but it's only one type of logical thinki…

>Mathematics and programming are not really all that related to each other and I think there's an overemphasis on the importance of math in programming for 99% of applications.

This is the standard thinking of someone who's not deep into math but deep into programming.

The two are deeply interrelated and in actuality are one in the same. Knowing math provides deeper understanding of programming. If you want to get better at programming in general, learning every new frameworks or specific technologies is not the path to getting better. Learning math is the path.

I cannot show you the path for you to understand it, you'll have to walk it yourself to know.

Suffice to say that there is an area of math that improves programming in a way you can understand. Type checking. Type checking proves that your program is type correct, it comes from math. You know it, and probably use it all the time.

To extend this, there's this concept of dependent types which also come from math. Dependent types can prove your entire program correct.

That's right with math you can write a single proof which is equivalent to billions of unit tests that touch the entire domain of test cases, to prove your program 100% correct. It's a powerful feature that comes from math. It's in the upper echelons of programming theory / mathematical theory and thus not trivial to learn. If you're interested you can check out the languages: Coq, agda or idris.

Re: Think in Math, Write in Code

#179

Post by crimsonalucard »

warent wrote: post #8

There's an unpopular and somewhat seemingly contradictory opinion that I have regarding this, because this isn't the first time I've seen this topic brought up. Mathematics and programming are not really all that related to each other and I think there's an overemphasis on the importance of math in programming for 99% of applications. Sure, mathematical thinking can be useful, but it's only one type of logical thinki…

Another Point: Math is basically taking a set of primitives/axioms and proving and constructing statements from that set of primitive axioms.

This is exactly what programming is.

Re: Think in Math, Write in Code

#180

Post by tonyarkles »

deadgrey19 wrote: post #139
chongli wrote: post #115

Earlier quoted context omitted.

What you're describing is a very limited view of math, resembling the general public view of math as being algebra, trigonometry, geometry, and calculus; that is, all the math people are exposed to in secondary school. Look further and you'll see disciplines such as mathematical logic, combinatorics, and graph theory, without which you wouldn't have networking or binary or computers at all, really. I don't know what…

What I'm discussing here is the general concept of modelling your program formally before writing it (as per the article). What I'm arguing is that this type of approach is only possible for a certain set of applications which take the form of y = f(x), where f(x) is some type of data transformation /computation operation (e.g. calculate the GCD of these ints, find the shortest path through a given graph, sort this s…

> this type of approach is only possible for a certain set of applications which take the form of y = f(x), where f(x) is some type of data transformation /computation operation (e.g. calculate the GCD of these ints, find the shortest path through a given graph, sort this set etc)

These days I'm trying to be mostly an embedded guy, and 100% understand what you're talking about re: problems that don't lend themselves well to mathematical modelling. Figuring out that your SPI bus is going slow because you've got the wrong multipler in a clock domain isn't a math problem :)

What I'd like to add to your y = f(x) examples though is that many Business Problems can (and probably should!) be modelled as y=f(x) type problems. I've seen a ton of business logic over the years that modifies objects in a pretty ad-hoc manner and is incredibly hard to reason about, especially in the big picture. The vast majority of the time, those problems can be modelled roughly as:

  new_state = f(old_state, event)
When you start modelling the business problems more formally like that, you can start using things like TLA+ to do model checking and find gaps in your formulation of the problem. Maybe you've got an state/event pairing that you haven't thought of. Maybe there's a way to get a model into a state that it can't escape from. TLA+ is useful for a lot more than verifying "calculate the GCD of these ints, find the shortest path through a given graph, sort this set", and I want to make sure people reading this don't write it off as a mathematical curiosity.

I've done a few embedded implementations that had pretty complicated state machines under the hood (off the top of my head, a LoRaWAN implementation). I modelled the states in TLA+, and it was a wonderful platform for discovering the flaws in the model I'd put together. It took a couple iterations before the model checker was happy, and from there the implementation was mostly mechanically translating my TLA+ model into code. There was some housekeeping stuff to keep track of (the TLA+ model was an abstraction), but it pretty much worked first try.

Post reply on HN