Live data from Hacker News

Think in Math, Write in Code

justinmeiners.github.io

161–170 of 256 posts

Re: Think in Math, Write in Code

#161

I spent more than 10years in Academia doing math. One thing I loved about this time, is that I was able to sit down anywhere and pound at my current research problems, without having any additional notes or books with me. Just pen and paper. Formal reasoning feels very empowering. You write down assumptions, apply transformation, arrive at conclusion. Proof one Lemma at a time. Work through some examples. Eventually…

Glad you liked it.

I mentioned in another comment, I am really emphasizing modeling the problem mathematically, not really using formal programming methods like lambda calculus. Sounds like you got my idea!

Re: Think in Math, Write in Code

#162
post #31

Earlier quoted context omitted.

But Haskell isn't math, it's code dressed up in a math costume.

Haskell is code (attempting to) implement category theory. It’s about as close to a programming language representing maths as we have (probably along with APL type languages)

My first language (not counting Basic or Fortran on punched cards) was APL, and my current language is Haskell. I'm a PhD mathematician. Luckily, I was trained far enough down the street from MIT to escape their Lisp world view, so we coded our computer algebra system in C, and it was fast enough to succeed and bring us tenure. Today, we'd choose Haskell.

Thinking in Haskell is the same feeling as thinking about math research. I know mathematicians who can only code in Haskell.

The trouble with discussing languages online is it's harder to assess if each party has actually used each language. The dogma in such discussions is completely "welcome to my world" familiar to me as a mathematician. We all have different opinions, and we're all sure we're right.

Re: Think in Math, Write in Code

#163
post #81

I honestly believe the majority of the problems in the industry comes from the refusal to treat programming as mathematics. Everything has to be "easy", so anyone can understand from a basic level. It's one of the reasons we don't like verifying software using TLA, coq(proofs for programs), refinement types or using functional programming techniques. "It's too difficult for the average programmer". The first excuse i…

Well, from a practical standpoint, it's more desirable to put out a partially-working system fast, which can be improved upon as it is live - than spend too much time planning and implementing a fully working system. Note: By partially and fully, I simply mean systems with more and less bugs. Rarely do companies and startups have the luxury to just lean back and take their time. It's a race against competitors, and e…

This is why I usually pitch formal specification as "you build your program faster and spend less time debugging it later." Framing it as a cost-saving measure over a "well ya GOTTA be correct" measure.

Re: Think in Math, Write in Code

#164
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

I may be wrong but I believe the Curry-Howard correspondence disproves your claim. One can translate between the two and find that they are equivalent.

The difficulty is that some programming languages are hard to model mathematically due to the way they were designed and implemented. Some, like Idris or Agda, make it easy to see the correspondences. Others like C or Javascript are harder.

The key to solving hard problems is being able to think concretely in abstractions. The best language we have for abstraction is pure mathematics.

Re: Think in Math, Write in Code

#165
post #30

I like that Python is quite close to my raw thoughts for simple problems. So writing an algorithm in Python almost feels like writing pseudocode. Heck, these days given an option between writing pseudocode and writing Python code, I choose Python for simple problems. Is there a similar programming language that makes mathematicians feel at home? Something that makes them feel that they would rather write their implem…

I’ve always been in the weak Sapir-Whorf hypothesis camp that your tools of expression influence and (sometimes) define your thoughts. A great example is the idea of matrices in math. Matrices don’t allow you to represent anything that a system of equations can’t. But it turns out that they are a very helpful tool and let you abstract over the problem space, much in the same way that higher order functions do. It’s e…

Can you describe some attributes of Ocaml and Racket that make them good contenders for expressing thoughts of mind?

Also is it Racket specifically that makes it a good contender or is it the fact that it is a Lisp that makes it a good contender? Would any other Lisp like Scheme or Clojure or Common Lisp be equally good?

Re: Think in Math, Write in Code

#166
post #60

Earlier quoted context omitted.

On the other hand the sculptor has considered the type of clay, the quantity, the tools she'd need to use to carve away those bits, and understands enough about what she wants to create to know what bits to carve away first. Programming may not be (all) math, but it's not art, either.

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.

Re: Think in Math, Write in Code

#167
I think there are languages and tools that mathematically minded programmers will find accessible enough and useful to aid them in their thinking. Dependently-typed programming languages such as Lean [0] and Agda [1] are both expressive enough to search for proofs to theorems and practical enough to execute programs.

And in the design space when we're thinking about problems of concurrency or liveness there are great tools like TLA+ that take a pure mathematical model and automate the checking that it satisfies our expectations. [2]

It's not all figures and drawings these days! I see maths and engineering integrating more closely in the future.

[0] https://leanprover.github.io/

[1] https://github.com/agda/agda

[2] https://lamport.azurewebsites.net/tla/tla.html

Re: Think in Math, Write in Code

#168

Thinking in math first has been the catch cry of functional programmers (and their formal logic/verification friends) for decades. And there's nothing wrong with it, unless the problem you are trying to solve actually requires performance. Then, you have to think in "system" first. For example: Write a program that captures network packets and stores them to disk as fast as possible . There's no maths to think of her…

This article is not about formal verification.

Why would mathematical thinking involve rejecting physical realities? If there is a performance constraint you are trying to optimize, account for it.

> Write a program that captures network packets and stores them on disk as fast as possible

How are you going to do that without formulas involving:

- network bandwidth - disk bandwidth - SATA bandwidth - packet ordering - compression time and ratios - amdahl's law

This sounds ripe for mathematical reasoning! Absolutely the way you model the problem is informed your knowledge of the hardware.

Re: Think in Math, Write in Code

#169
post #126

Earlier quoted context omitted.

For most programs, you can just use PlusCal instead of straight TLA+ and get most of the benefits. Unless you're writing something that is heavily concurrent or distributed.

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".

Re: Think in Math, Write in Code

#170

I think that the total programming man hours spent on writing pure math computation would be dwarfed by the much larger number (I think) spent on doing menial computation: fetching data, transforming it and sending it forward/rendering some output. I suppose this article is targeted at that privileged former group.

See my example. It was very short and helped me clarify immensely what I was going to write.

You're right that if I am going to add another template to a Django site, there isn't much math to think about. But anything bigger than that, there are always questions worth considering.

Post reply on HN