Certigrad: bug-free machine learning on stochastic computation graphs

Post by kg9000 » Mon, Jul 10, 2017, 8:45 PM UTC

Post by taneq » Mon, Jul 10, 2017, 10:57 PM UTC

binarymax wrote: post #2

Meta to the Certigrad project, for those mystified by the 'lean' programming language, here is a good start: https://leanprover.github.io/programming_in_lean/programming...

Post by taneq » Mon, Jul 10, 2017, 11:07 PM UTC

Post by fchollet » Tue, Jul 11, 2017, 12:28 AM UTC

ogdan wrote: post #6

taneq wrote: post #5

I find the appeal of formally proven languages somewhat confusing. All you're doing is moving the bugs from the source code to the specification. (Alternately, you can think of source code as a 'specification' for a compiled program. You still have to transfer the same amount of information to the computer.)

The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct.

Post by Eridrus » Tue, Jul 11, 2017, 12:58 AM UTC

taneq wrote: post #5

I find the appeal of formally proven languages somewhat confusing. All you're doing is moving the bugs from the source code to the specification. (Alternately, you can think of source code as a 'specification' for a compiled program. You still have to transfer the same amount of information to the computer.)