[urthor]

How often do proofs come up in industry though?

Usually I find proofs are what you bring in the consultant for.

I'm not going to hand on heart vouch for anything like that as a generalist.

Combinatrics, Big O and set theory absolutely. Everyone is far better off with those.

[mcguire]

Computer programming is applied formal logic. No, really, it is. I'm completely serious.

[hnfong]

You can reassert this tautological statement all you want, but when AI-assisted programming tools start compiling pseudo-natural-language into C++, you'd better accept the fact that either:

1. The definition has no bearing to what's happening in the real world, or

2. "Computer programming" ceases to exist as a productive activity and you need to invent a new name for AI-assisted programming.

[mcguire]

But that is part of the point: there is no programming tool to compile natural language into code. Instead, a programmer has to convert the natural language into a formal language that a compiler can deal with. You know all those nifty refactoring tools? They're treating the program as a construct in a formal language---they can make specific changes without altering the meaning.

Oh, and there is nothing tautological about it, at least as far as most programmers seem to work.

[hnfong]

> no programming tool to compile natural language into code

Pretty sure you missed a couple news articles recently...

https://news.ycombinator.com/item?id=30179549 https://news.ycombinator.com/item?id=27676266

They're not exactly reliable, but you probably could say the same for the earliest compilers (from programming languages to asm/machine code).

I'm not saying they will definitely be usable in the short term future, but that future is probably coming sooner or later, and I don't think a fragile definition (programming==="applied formal logic") is worth reiterating over and over again as if it were some fundamental truth.

[MaxBarraclough]

I don't think anyone is going to dispute that though, except perhaps on a point of detail: it took Hoare logic to bridge the gap between imperative programming and 'ordinary' mathematical logic.

If I'm reading them right, urthor's point is that the average programmer doesn't directly benefit from being skilled in developing formal proofs about code. (I rambled at some length on this topic recently. [0]) Very few software development workplaces value correctness so highly that they invest in formal methods.

That said, I think the case can be made that learning about formal methods is useful in instilling a sense of how rigorous software development can be, and perhaps to develop a healthy contempt for hand-wavy sloppiness. Perhaps it's also helpful to learn that informal requirements, formal specifications, and implementations, are three different things. I think this may be true even if we rarely use formal specifications in practice.

[0] https://news.ycombinator.com/item?id=30000146

[roenxi]

Breathing is applied formal logic. The range of things that can be reduced to applied formal logic is pretty much everything if we accept that "applied formal logic" doesn't mean formal mathematical proofs.

If we could strip out of reality the bits that can be understood as a practical application of the basic branches of math there wouldn't be anything left. Nevertheless most people get a long way in life without needing to engage with that (which is lucky because there is too much to learn in one lifetime).

[baq]

I get the OP’s point: it doesn’t matter what you think about usefulness of knowing how to formally prove anything, the point is that you’re doing it every time you program a computer, so might as well 1) be aware of that 2) learn a thing or two about how it’s done by pros.

[roenxi]

Should I study knot theory to tie my shoelaces? Should tailors and cup-makers study topology? Should it be mandatory to study economics before buying groceries?

Looking at code as applied formal logic is not a useful view outside of some rather obscure communities. Even code as a recipe is more useful view in practice.

[baq]

I’m not saying you should get a phd in logic. I’m saying knowing what your inputs and outputs are supposed to be and writing test assertions is basically checking whether your theorem/lemma is true in disguise (unit of code works as expected) and knowing a bit of theory from that domain can’t hurt. Even if it’s only de Morgan’s laws, which you’ll admit is a rather low bar…

[roenxi]

> writing test assertions is basically checking whether your theorem/lemma is true in disguise

But that is almost the polar opposite of treating a program as applied logic. If there is one thing that is not reasonable when dealing with logic, it is "proof by multiple test cases that seem to work, I think".

And I don't clear the low bar for de Morgan’s laws, I've completely forgotten what they are. And on looking them up, that doesn't look like an important component of programming. A programmer could reasonably get away with not knowing them. Probably going to learn them by rote over a few years, but that is hardly "applied logic" in any sense that is worth talking about.

[mechanical_bear]

Computer Science isn’t about industry. If you are dead set on being the best in industry go take an Information Systems degree, or similar.

[urthor]

I think if computer science degree weren't about industry, there'd be far fewer terminal undergraduates floating around the world.

If people came for the science, everyone would ride off, discover something, and get a PhD.

I just see formal proofs as something you get a genuine scientist to do. If you're someone focused on rigorously correct proofs, you get a rigorous PhD.

I don't pretend that I'm up for that, or that I'm qualified to produce quality work in that space.

But I also don't believe any of my fellow terminal undergraduates are the right sort of people to do this work.

Let's face it, we all had a close encounter with the mathematical proofs, and ran in the other direction as fast as we could!

[mechanical_bear]

I didn’t run, I double downed lol. CS Piled High and Deeper here…