Bob Harper wrote a really good blog entry that expounds on this as Computational Trinitarianism [1].<p>Michael Shulman also wrote about the extension to Homotopical Trinitarianism [2]<p>For a good summary with links there is [3]<p>[1] Computational Trinitarinism, <a href="https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/" rel="nofollow noreferrer">https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...</a><p>[2] Homotopical Trinitarinism, <a href="http://home.sandiego.edu/~shulman/papers/trinity.pdf" rel="nofollow noreferrer">http://home.sandiego.edu/~shulman/papers/trinity.pdf</a>]<p>[3] nCatLab, <a href="https://ncatlab.org/nlab/show/computational+trilogy" rel="nofollow noreferrer">https://ncatlab.org/nlab/show/computational+trilogy</a>
Could 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?
Programming in dependent types with univalence (Homotopy Type Theory) is an awesome way to see this realized.<p>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.
Lamport’s <i>Computation and State Machines</i>[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).<p>[0] <a href="https://research.microsoft.com/en-us/um/people/lamport/pubs/state-machine.pdf&type=exact" rel="nofollow noreferrer">https://research.microsoft.com/en-us/um/people/lamport/pubs/...</a>
If you want to see how the Curry-Howard isomorphism works in practice, this is a very accessible introduction: <a href="https://groups.seas.harvard.edu/courses/cs152/2021sp/lectures/lec15-curryhoward.pdf" rel="nofollow noreferrer">https://groups.seas.harvard.edu/courses/cs152/2021sp/lecture...</a>
Not 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.<p>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.
Okay. Today I'll be the idiot.<p>I don't get it. Or rather, I don't get the significance of the Curry-Howard Isomorphism. Questions:<p>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?<p>2) Are the "programs" referred to here to merely pure functions (i.e. side effect-free, global state-free ones)? It <i>sounds</i> like it is based on lines like this:<p>>When a computer program runs, each line is “evaluated” to yield a single output.<p>That ... seems to cram "computer programs" into some kind of Procrustean bed <i>unless</i> we're taking about pure functions. But then it also talks about how CHI has applications in verifiable programs, which, I'm told, <i>can</i> reason about side effects.<p>Feel free to call me an idiot, as long as you can also inspire an aha-moment.
On 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.<p>ps. and our calculators (& excel) needs better support for it
I don't know that much about it, but the impression I got from studying TLA+ was that machine-executable code was distinctly <i>not</i> 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.
A link between equations and programs is show in this video: <a href="https://m.youtube.com/watch?v=aAlR3cezPJg&pp=ygUHU2ljcCA3YQ%3D%3D">https://m.youtube.com/watch?v=aAlR3cezPJg&pp=ygUHU2ljcCA3YQ%...</a><p>I assume mostly known in this site.
In 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?
Most overrated correspondence ever.<p>You don't need curry-howard for software verification, you don't need it for mathematics, and you don't need it for logic.<p>You only really need it to j*rk off hard over types.
Yes, of course there is a link.<p>At the lowest machine level, a computer program is simply base 2 math --- the simplest possible number system --- aka binary logic.<p>Aside from moving mathematical data around in storage, math is really about the *only* thing a computer processor does.
This is very old.<p>Yes, programming is a super set of theorem proving.<p>It is true, but not generally useful.<p>Building useful programmes is, IMO, best described as a craft. It is learnt from other crafters, and improves with practice<p>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