3 ms·

I'm also interested to see how the worlds of program synthesis (specifically type directed, proof-checking, dependently typed stuff) can combine with deep lear

I'm also interested to see how the worlds of program synthesis (specifically type directed, proof-checking, dependently typed stuff) can combine with deep learning. If recent neural nets have such great results on large amounts of unstructured data, imagine what they can do with a type lattice.

gtani 9y ago
Recent baby steps in gradient checking: https://news.ycombinator.com/item?id=14739491 https://news.ycombinator.com/item?id=14739491