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

Logic for Programmers

logicforprogrammers.com

Post reply on HN
Print view View original

51–53 of 53 posts

Re: Logic for Programmers

#51

Post by deterministic »

layer8 wrote: post #46
leonidasrup wrote: post #37

Earlier quoted context omitted.

Constructing a formal proof is not only related to programming, it's the same thing. Curry–Howard correspondence: "In programming language theory and proof theory, the Curry–Howard correspondence is a direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation." h…

It’s not the same thing, in particular if you work in a dynamically-typed programming language, have mutable state, parallelism, and infinite loops. The Curry–Howard correspondence only applies in a limited sense to practical programs. That’s why you can have a productive programmer who is nevertheless unable to construct valid proofs. (I’m very much in favor that programming should involve proofs as much as possible…

Not true. seL4 (for example) is an example of a real time kernel proven correct end-to-end and used on millions of devices.

Another example is CompCert (a proven correct C compiler used by Airbus and others for real production software).

Re: Logic for Programmers

#52

Post by LudwigNagasena »

js8 wrote: post #36
LudwigNagasena wrote: post #33

Earlier quoted context omitted.

> I feel like no serious work with this ambition What ambition? The book is an applied introduction for people who aren’t even familiar with what ∃ means. It’s 200 pages, which is at best comparable to a semester-long course.

Ambition to help programmers understand logic and how it relates to their discipline. But maybe you're right, it cannot be (currently) done in 200 pages, although I hope somebody proves that wrong. It kinda reminds me of the debate whether functional programming is suitable for beginners, despite being simpler than imperative, while imperative is more familiar. I am opposed to familiarity argument (I think classical…

I don't see much value in knowing that dependent types can be used to encode logical quantifiers or similar stuff in applied programming. Maybe there is actual value that it creates after you grok those concepts (beyond the general applicability of any concept or metaphor in your thinking), but I don't see it.

"Functional programming" in applied programming usually just means using less mutable state and using stuff like `map` and `reduce` to make semantics of code more predictable and move the burden of optimizing actual implicit mess it creates to compiler/interpreter.

Post reply on HN