28 ms·
The deep link equating math proofs and computer programs
- qsort 3y agoIf you want to see how the Curry-Howard isomorphism works in practice, this is a very accessible introduction: https://groups.seas.harvard.edu/courses/cs152/2021sp/lectures/lec15-curryhoward.pdf https://groups.seas.harvard.edu/courses/cs152/2021sp/lecture...
- _a_a_a_ 3y agoAccessible for who, do you mean? That is in no way 'accessible' without solid exposure to quite a lot of discrete maths (which I have and it's still hard going). λf :(τ 1 × τ 2 ) → τ 3 .λx:τ 1 .λy:τ 2 .f (x,y) has type ((τ 1 × τ 2 ) → τ 3 ) → (τ 1 → τ 2 → τ 3 ). Yeah, that's accessible.
- fooker 3y agoSeems accessible, if you're willing to look up what what you don't understand.
- _a_a_a_ 3y agoOh get real. I have a background in this. Lambda notation, Hoare notation (I think), 'standard' logic notation. Don't talk rubbish about 'look it up'. You need a degree to get this. Not a metaphorical degree, the real thing. Edit - and a brain bigger than mine.
- the_af 3y ago> Don't talk rubbish about 'look it up'. You need a degree to get this. Not a metaphorical degree, the real thing. You really don't need a degree. The Curry-Howard isomorphism is taught in undergraduate CS courses, to students who are simultaneously being introduced to lambda calculus. While I wouldn't say it's trivial, it's not rocket science either. Most students get it and pass the exams.
- fooker 3y agoIt's an introductory CS concept, requiring a degree would make things a bit circular...
- SilasX 3y agoUnder that constraint, what wouldn't count as an accessible exposition?
- user3939382 3y agoIt doesn’t matter what you think is accessible, it only matters if the person trying to access it thinks it’s accessible. I don’t.
- the_af 3y agoIf you can learn how to program, you can learn how to understand this. You first must learn the notation, just as when you learned "def", or "func", or "[x for x in ...]", or "int main() { ... }", or whatever your favorite language's notation is. "Accessible" doesn't necessarily mean "with just knowledge of English, you can jump to this example and immediately understand what it means". Some work is always required; accessible just means this work is not too hard. For example, Python's notation has been occasionally described as "accessible", yet I wouldn't expect my mum to immediately understand a non-trivial Python snippet (so no "print('hello')") without any previous explanations.
- _a_a_a_ 3y agoQuiz: what is the opposite of patronising? Because that's what you're being. Not talking down to people but assuming more than is typical. You're clearly highly intelligent, evidently more so than I am. Additionally my mind doesn't work like yours, I'm not an abstract thinker. Plonk stuff like this in front of me and I can decipher it eventually, if I can get some clear statement of the notation and its semantics anyway, and there is stuff in there I'm not familiar with. Most people aren't abstract thinkers. They are motivated by practical concerns. I spent an enormous amount of time reading up on stuff like this and I really can't see the value to it to me as a programmer. It's deeply frustrating because I know it has value, but I just can't use it. It's interesting, I know it's useful, but I can't use it. Please allow that other people think differently and are motivated differently, and don't assume that what's easy for you is for them. I wish I had your cranium.
- zozbot234 3y ago> Most people aren't abstract thinkers. They are motivated by practical concerns. Abstract thinking is motivated by practical concerns, namely being able to think comfortably about larger problems without being limited by one's capability for complex reasoning. Most people don't do it because they aren't used to, or they have never been taught how.
- seanhunter 3y agoBy that definition "Baby Rudin"[1] is an accessible introduction to analysis as long as you're willing to look up what you don't understand (ie everything probably the first time) in some other source. [1] https://maa.org/press/maa-reviews/principles-of-mathematical-analysis https://maa.org/press/maa-reviews/principles-of-mathematical...
- fooker 3y agoRudin is not accessible if you're just looking up things. But it is if you have someone to explain stuff when you get stuff. This one doesn't need that.
- qsort 3y agoIt's accessible to anybody with any experience programming and who is willing to pay attention. You are just taking a formula out of context, omitting the plain English explanation that comes before it, and pretending it's some kind of alien math. It's not scary at all, in fact it's very simple. Let's do this in Python. First, write a function that curries: def curry(f): def g(x): def h(y): return f(x, y) return h return g my_func = lambda x, y: 10 * x + y curried = curry(my_func) print(curried(5)(3)) # output: 53 Now, let's type it in such a way that mypy --strict won't complain: from typing import TypeVar, Callable A = TypeVar('A') B = TypeVar('B') C = TypeVar('C') def curry(f: Callable[[A, B], C]) -> Callable[[A], Callable[[B], C]]: def g(x: A) -> Callable[[B], C]: def h(y: B) -> C: return f(x, y) return h return g What's the type of curry? Let's hover our cursor over the function name, and lo and behold: Callable[[Callable[[A, B], C]], Callable[[A], Callable[[B], C]]] That's it. That's all it's saying.
- _a_a_a_ 3y ago> You are just taking a formula out of context, omitting the plain English explanation that comes before it, which, this? "We saw earlier in the course that we can curry a function. That is, given a function of type (τ 1 ×τ 2 ) → τ 3 , we can give a function of type τ 1 → τ 2 → τ 3" That helps no-one unless you have some serious hand-holding. I know the type of curry, I've written curry/bind/whateveer in C#, scala, JS and likely others. I have a background in this. It's not 'accessible' to mere mortals and even I'm not familiar with some of the notation here. Stop pretending it's just laziness on other people's part. (oh yeah, did I forget to put constructive logic in my list above? Brouwer's intuitionism? FFS get real, I never even heard of that until a few years ago)
- zozbot234 3y agoIt is accessible if you know a few bits of syntax, such as → being right-associative so τ1 → τ2 → τ3 means τ1 → (τ2 → τ3). And others such as "f: X → Y declares f as a function from X's to Y's." which you can find in any math textbook. The point of using such a terse notation rather than faffing around with Callable[…] is to make it possible to work with larger examples without getting bogged down in the verbiage. It's why we use symbols to solve equations in K-12 math.
- mrkeen 3y agoIt's just the 'mathy' type-setting which is hard to read. Types and terms are in the same font & colour and they're on the same line. To paraphrase: You can curry a function (supply its arguments one-by-one instead of all at once). You have: f(x, y) which has type (τ1 x τ2) -> τ3 You want: f x y which has type τ1 -> τ2 -> τ3 Here's a function which converts what you have to what you want: λx. λy. f(x, y) It has type: ((τ1 × τ2) → τ3) → (τ1 → τ2 → τ3) This type "Curry-Howard"s to the logical formula: (A ∧ B ⇒ C) ⇒ (A ⇒ (B ⇒ C)) Since this logical formula is a tautology, the above conversion function preserves the meaning of the function it converts.
- _a_a_a_ 3y ago> (A ∧ B ⇒ C) ⇒ (A ⇒ (B ⇒ C)) > Since this logical formula is a tautology You forgot to say 'obviously' /s
- housecarpenter 3y agoI would interpret "accessible" here as meaning relatively accessible compared to what it could be. The underlying concept is inherently difficult, and so it will always be somewhat inaccessible, but within the space of all possible explanations, I would agree that it's on the more accessible end rather than the less.
- xelxebar 3y agoNifty. That was a nice 4-page exposé of the correspondence. There are no general proofs, but the correspondence between notations is very suggestive and invokes interesting intuitions, I think. The example derivations with the uncurry example are quite fun to work through. The paragraph about continuations corresponding to double negation is also super neat! Now I just wish there were something similar for the missing category theory third of the trinitary mentioned in another comment.
- caycep 3y agowas this something to do with Djykstra's work?
- maleldil 3y agoJust a head's up, there's an easy way to remember Dijkstra's spelling: D ijk stra. You know, ijk as the common loop indices.
- Scarblac 3y agoAlso, think of ij as a single letter, quite like a y but with dots.
- smokel 3y agoAlso, Dijkstra was from The Netherlands, and the word "dijk" is Dutch for dike, i.e. the water barrier. "Dikestra" has a shorter path to the Dutch pronunciation than Djikstra.
- klyrs 3y agoI've always thought the ijk were quaternions and the alternative spelling would be D-1stra.
- wisnesky 3y agoYes, although Dijkstra was interested in proving programs correct in general, not just in how lambda calculi correspond to logics correspond to categories (a proof technique for program correctness, among other things).
- boxfire 3y agoProgramming in dependent types with univalence (Homotopy Type Theory) is an awesome way to see this realized. The typing statement has to be proven by realizing the isomorphism demanded by substitution. You are more than anything directly proving what you claim in the type. Since proof is isomorphism here, the computation in terms of lowering the body of the definition to a concrete set of instructions is execution of your proof! (possibly machine code or just abstract in a virtual machine like STG). The constructive world is really nice. I hope the future builds here and dependent types with univalence is made easier and more efficient.
- js8 3y agoWhat specific system (programming language) do you recommend to try this?
- codekilla 3y agoFor dependent types, I would look at Idris [1]. Adding Univalence in a satisfying way is I think still somewhat of a research question (I could be wrong, and if anyone has any additional insight would be interested to hear), i.e. see this thread about Univalence in Coq [2]. There are some implementations in Cubical Type Theory, but I am not sure what the state of the art is there [3] [1]https://www.idris-lang.org https://www.idris-lang.org [2]https://homotopytypetheory.org/2012/01/22/univalence-versus-extraction/ https://homotopytypetheory.org/2012/01/22/univalence-versus-... [3]https://redprl.org https://redprl.org
- haltist 3y agoIt should be possible to embed cubical type theory in Idris.[1][2] 1: https://arxiv.org/abs/2210.08232 https://arxiv.org/abs/2210.08232 2: https://chat.openai.com/share/aadb7a0a-08a4-4951-b877-cb2f6138fa45 https://chat.openai.com/share/aadb7a0a-08a4-4951-b877-cb2f61...
- AnimalMuppet 3y agoThis is not going to catch on any time soon. Assume that regular software has, on average, one bug every 50 lines. (All numbers made up on the spot, or your money back.) Let's suppose that Idris can reduce that to absolutely zero. And let's suppose that totally-working software is worth twice as much as the buggy-but-still-mostly-working slop we get today. But Idris is harder to write. Not just a bit harder. I'd guess that it's maybe 10 times as hard to write as Javascript. So we'd get better software, but only 1/10 as much of it. Take your ten most favorite web applications or phone apps. You only would have one of them - but that one would never crash. Most people won't make that trade. Most companies that produce software won't make it, either, because they know their customers won't. Well, you say, what about safety-critical software? What about, say, airplane flight control software? Surely in that environment, producing correct software matters more than producing it quickly, right? Yes, but also you're in the world of real-time embedded systems. Speed matters, but also provably correct timing. Can you prove that your software meets the timing requirements in all cases, if you wrote it in Idris? I believe that is, at best, an unsolved problem. So what they do is they write in carefully chosen subsets of C++ or Rust, and with a careful eye on the timing (and with the help of tools).
- athrowaway3z 3y agoOn a tangent. I think its worth it to push typed mathematics waaaaay down into highschool. While students are learning multiplication, the teaching tools/question/answers need to teach how that changes the result's units (types). Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test. ps. and our calculators (& excel) needs better support for it
- carbocation 3y agoWhen I was in high school units were a key part of science education. Is this no longer the case? Your point about tools that support units is great. Reminds me of https://frinklang.org/ https://frinklang.org/
- Jtsummers 3y ago> Highschool physics especially needs to have 'proper units at every stage of calculation' as part of the test. I can't imagine any HS science class not already doing this. It would be impossible to answer many, if not all, of the questions correctly if you mix units (either unit-kind like mixing time and distance units, or unit-scale like mixing seconds and hours).
- euroderf 3y agoNor possible to write literately about energy issues.
- seanhunter 3y agoMost maths teaching emphasises this but they don't talk about it in quite the same way. Units are dealt with as units whenever you are doing real world problems around velocity, speed, physical quantities etc and you are taught not to mix units, and how units "cancel" etc each other when you deal with exponent laws. Types as such are dealt with as sets. So for example I'm working my way through Serge Lang's "Basic Mathematics" at the moment[1], and it starts with the natural numbers, then the positive integers, then the integers, then the rational numbers, then the reals etc. This is very normal for high-school level maths education. I believe that mathematically the formal theory of types comes from a different branch from sets which arose when Russel attempted to address the problems caused by his paradox. "Type" theory was part of Russel's solution whereas Zermelo Fraenkel set theory is where everyone else felt that sets just needed a little patch to carry on working pretty much as before. [1] Which I'd really recommend for anyone who wants a maths refresher that starts from very basic concepts but really challenges you to think like a mathematician, prove things etc. So in the first chapter when you only know the distributive and associative properties he has you using them to prove stuff.
- jqpabc123 3y agoYes, of course there is a link. At the lowest machine level, a computer program is simply base 2 math --- the simplest possible number system --- aka binary logic. Aside from moving mathematical data around in storage, math is really about the *only* thing a computer processor does.
- codekilla 3y agoBob Harper wrote a really good blog entry that expounds on this as Computational Trinitarianism [1]. Michael Shulman also wrote about the extension to Homotopical Trinitarianism [2] For a good summary with links there is [3] [1] Computational Trinitarinism, https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr... [2] Homotopical Trinitarinism, http://home.sandiego.edu/~shulman/papers/trinity.pdf http://home.sandiego.edu/~shulman/papers/trinity.pdf] [3] nCatLab, https://ncatlab.org/nlab/show/computational+trilogy https://ncatlab.org/nlab/show/computational+trilogy
- akomtu 3y agoTo the Mr. Harper's observation we should add that the trinitary theory of computation needs to express itself in reality and it does so thru the quadrant of hardware: transistors, memory, electricity and machine code. Thus three, standing on the four, represents computation in action.
- nradov 3y agoIn principle it doesn't have to be transistors specifically. Any switching device will suffice.
- deleted 3y ago[deleted]
- gnufx 3y agoLacking time to study, is this basically what Phil Wadler has written and talked about, like "Propositions as types"?
- SilasX 3y agoOkay. Today I'll be the idiot. I don't get it. Or rather, I don't get the significance of the Curry-Howard Isomorphism. Questions: 1) Is there an example of a proof and its corresponding program that makes you say "whoa, trippy, I didn't expect those to be related"? Like, yeah, an Int -> Boolean function "proves" you can construct a Boolean from an integer, but ... so what? What would a non-trivial proof (say, on the order of the Pons Asinorum) look like as a program? 2) Are the "programs" referred to here to merely pure functions (i.e. side effect-free, global state-free ones)? It sounds like it is based on lines like this: >When a computer program runs, each line is “evaluated” to yield a single output. That ... seems to cram "computer programs" into some kind of Procrustean bed unless we're taking about pure functions. But then it also talks about how CHI has applications in verifiable programs, which, I'm told, can reason about side effects. Feel free to call me an idiot, as long as you can also inspire an aha-moment.
- zmgsabst 3y agoThere are only side effects! When you compute a pure function, you’re still physically manipulating registers, cache, etc. You can use the proof-program perspective to formalize reasoning about a program: - you have some domain model; this expresses the “business logic” of your software - you have an abstract model, in a category for your programming language; this expresses an equivalent structure as the “business logic” - you have a concrete model, in a category for your hardware; this expresses an equivalent structure as it gets executed Reasoning about the translations between these steps, their properties, etc is why you want to connect software to proofs. For example, if you want to find an optimal implementation: you want the shortest path of atomic arrows in your hardware category, which corresponds to the desired computation in your language category. Category theory is the language in which we connect our theory of hardware to our theory of the business domain!
- zozbot234 3y agoInt -> Boolean is just the type of any arbitrary decidable property on Int's, so it's not very useful on its own. But if you can endow your Int -> Boolean function with a proof that it computes some property you actually care about, that's more likely to be helpful. The proof itself need not even be constructive, since the requirement for constructibility was taken care of by providing the code for that function. Constructibility becomes more of a big deal if you want to be able to compose constructive proofs, or write proofs that rely on instances of some other proof as input, since then the strategy of providing some construction as a bare algorithm and separately proving it correct may run into problems. And if your return type is something other than Boolean, that represents some more general construction rather than mere decidability. But everything else is just about the same. Of course this all assumes a total language with no general recursion, since otherwise you can "prove" anything by just looping forever and not delivering a result.
- samirillian 3y agoI don't know that much about it, but the impression I got from studying TLA+ was that machine-executable code was distinctly not mathematics, and that programs are never provable. Am I wrong? Or is this just the kind of sensational snake-oil that HN readers are susceptible to buying.
- bluGill 3y agoMost code is so complex that even with the aid of a computer we couldn't run a proof on it if we tried. Most (all!) code also has bugs so if we tried to prove it we would instead prove it doesn't meet requirements. However the theory itself allows that all code could be mathematically proven if you can work around those two issues. It also isn't clear that the machines itself actually do what they say, though hardware is a lot more likely to be mathematically proven.
- staunton 3y ago> hardware is a lot more likely to be mathematically proven Maybe that's a nitpick, but I would say it's fundamentally impossible to mathematically prove anything at all about a physical system. You have to assume some model to do the proof and have no way of ever "proving" (what would that even mean?) that model. I guess you're referring to the fact that verification and formal methods are used in hardware more often than software. This is due to commercial reasons: you can't just reprogram a million chips once they leave your fab.
- Tainnor 3y agoWe run proofs on code all the time, it's called type-checking. What you mean is that it's practically infeasible to verify every program behaviour we're interested in. That's probably true for large enough programs, but it doesn't mean we can prove nothing about them.
- kaba0 3y ago> However the theory itself allows that all code could be mathematically proven I don’t think this is true, something as “trivial” as halting already can’t be proven in the general case.
- ewuhic 3y agoCould anyone suggest a happy path ("zero to hero") book on formal verification, which also does the ecosystem review for the formal verification languages, and then focuses on one, as well as provides the reasoning and mentions tradeoffs for such a choice?
- miloignis 3y agohttps://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ is a great zero-to-hero resource (it's what I used), but to my knowledge it doesn't have an ecosystem review in it. It uses Coq, but the first book has been ported to at least Isabelle, if not others.
- blueberry87 3y agoAlso agda: https://plfa.github.io/ https://plfa.github.io/
- noqc 3y agoSince the whole premise here is that formally verifying the properties of programs is equivalent to constructive mathematics, I think you might be asking for too much, modulo your definition of hero.
- bruce343434 3y agoWhat do you mean by modulo here?
- tux3 3y agoIt means except for X, or disregarding X If you have a particularly generous definition of hero, then you might not be asking too much
- rsrsrs86 3y agoThere is no such thing as zero to hero for formal methods. It’s a dense and difficult field.
- f1shy 3y agoA link between equations and programs is show in this video: https://m.youtube.com/watch?v=aAlR3cezPJg&pp=ygUHU2ljcCA3YQ%3D%3D https://m.youtube.com/watch?v=aAlR3cezPJg&pp=ygUHU2ljcCA3YQ%... I assume mostly known in this site.
- auggierose 3y agoMost overrated correspondence ever. You don't need curry-howard for software verification, you don't need it for mathematics, and you don't need it for logic. You only really need it to j*rk off hard over types.
- strogonoff 3y agoLamport’s Computation and State Machines[0] is an interesting take on relating mathematics to computer programming. Lamport appears to treat programs as state machines, making it possible to reason about those with pure mathematics (in a way independent of programming language syntactic constructs). [0] https://research.microsoft.com/en-us/um/people/lamport/pubs/state-machine.pdf&type=exact https://research.microsoft.com/en-us/um/people/lamport/pubs/...
- zozbot234 3y agoYou can also express the "programs as state machines" view in terms of programming language constructs, namely monads (for Time, State and Non-Determinism). If you take a strictly mathematical view of the topic you'll call these 'modalities' or 'modal operators' instead but it's the same deal.
- amw-zero 3y agoThis is my favorite CS paper of all time. Reason being, it distills multiple different areas of CS down to one idea: state machines. Now I'm frequently able to map a complex idea down to a state machine, which makes all kinds of problems more manageable.
- worik 3y agoThis is very old. Yes, programming is a super set of theorem proving. It is true, but not generally useful. Building useful programmes is, IMO, best described as a craft. It is learnt from other crafters, and improves with practice Formal methods can be helpful in specific cases but generally speaking writing correct formal specifications is just as hard, or harder, than writing useful, reliable, computer programs
- passion__desire 3y agoCraft similar to painting which AI has overtaken. What we consider programming will go the similar route.
- gorgoiler 3y agoNot just formally but also stylistically. Composable lemma and composable functions are two leaves of the same book. The construction of a proof is to convince the reader of the correctness of the logic and this is exactly the same goal of a mathematical author as it is of a computer programmer. Business really interferes with the goal of the mathematical programmer — proofs of concept, hacks to get MVPs over the line, throwaway demos to investors etc. — but after a certain point the value of the codebase becomes entrenched into the value of the business and that’s when you need to bring in the mathematical coders to constantly refine and prune your codebase into something that will survive and bear out the earnings per share values.
- bigmattystyles 3y agoDon’t languages like ADA take this literally and require that your instructions be mathematical correct / complete?
- Jtsummers 3y agoAda, not ADA, it's never been an acronym. And no. Ada is an imperative language with an expressive type system (especially compared to other imperative languages). But it doesn't require things like mathematical correctness/completeness. You may be thinking of SPARK which is a subset of Ada that uses contracts and a prover to prove the contracts hold.
- thyrsus 3y agoThe barber was a woman.
- ewuhic 3y agoIn addition to my other comment here, is there any application of formal verification for complex ETL (Data) pipelines, from the standpoint of enumerating transformations, workflow steps, and states, with less emphasis on temporal soundness?
- pas 3y agomy first thought was something something dependent types (Idris, Agda), but it also sounds like TS-like structural typing with a Rust-like Result type. proving that every incoming message is either parsed correctly or we return an error seems to be the basic building block. and then every transformation should be other pure functions. thought I guess you mean something more top-downish? for that there's "program interpretation" ( https://github.com/AdrielC/free-arrow https://github.com/AdrielC/free-arrow ) and this just looks very interesting https://deepai.org/publication/a-coq-based-synthesis-of-scala-programs-which-are-correct-by-construction https://deepai.org/publication/a-coq-based-synthesis-of-scal...
- throwthrow5643 3y agoHow to formally verify a single page web application?