Hacker News Reader

Comment by mrcactu5 | Hacker News Reader

i am having my doubts these days.

i would like to read my programs as proofs. then I ask myself what is the Amazon.com front page proving?

we talk about proof writing in Haskell or Agda. What about Python? Can we prove things there?

And finally I think about the statements I would actually like to prove? Much of mathematics requires second order logic or beyond, such as the Fundamental Theorem of Calculus.

So for me the triad between Math and Logic and Computer Science is less than air-tight and will remain that way.

View on HN

The Amazon.com front page generating code is a proof relating some properties of its output to its input and that it halts. However it's also basically incomprehensible, so I doubt anyone alive could actually tell you precisely what it's proving.

Your ability to prove something in any language is dependent on having a formal semantic for that language, or at least for a cognitively manageable subset that you're willing to restrict yourself to. The language semantics and memory model serve as axioms.

Given how American programmers are trained, it's not realistic to expect them to be able to think of programs in a logical semantic way. There is something of an art to it and it's hard to learn a new way of thinking when you're satisfied with a way you already have.

I agree that you can have an enjoyable hobby or make a living programming without really understanding what you're doing beyond intuitively and that's totally fine. Computing time is cheap and most applications don't cause any great harm when they behave in unintended ways. However the isomorphism between predicate calculus and computer programming isn't subjective. Programs really are proofs, just some of them are very sloppy.

Amazon's front page proves that by typing in the amazon.com url, you get a page of whatever content amazon generates. Which isn't a very useful proof.

Python is dynamically typed, so it doesn't prove much either. But in a statically typed language, if you have a method that takes an integer and returns a string, then you have proven you can generate a string from an integer. If it runs, then you have proven it. Granted, that's also not particularly useful, but it's proven if it compiles/runs.

To prove, you need types. Typeless proofs/programs are just really general, not-very-useful proofs, same with dynamic typing. That's why static typing gets you a little closer to the correspondence/isomorphism.

Dependent types gets you closer still - like, if you have a method that will only compile if the method takes an array of numbers, and returns only the subset of those numbers that are even - then the correspondence is starting to get a bit useful. Then you know your output won't have numbers that weren't in the input.

I don't have much experience with this so I'm probably explaining it badly.

Reply on news.ycombinator.com