I met some interesting gradual type people at POPL yesterday, and the schedule was full of good talks!
Friday opened with a great introduction to probabilistic PLs with live demos. It showed usage, although it feels like "random programming with magic"
miniblog.
How do you do program synthesis when the user hasn't given enough examples? You find perturbation properties (e.g. change input => change output) to generate more examples!
Tons of great talks at #POPL yesterday:
I loved this approach to solving the expression problem, building a PL and tool where you could toggle between data and codata (like functions/methods)! https://popl20.sigplan.org/details/POPL-2020-Research-Papers/57/Decomposition-Diversity-with-Symmetric-Data-and-Codata (had a live demo!)
I attended a bunch of great talks at #POPL yesterday.
My highlight yesterday was a delightful talk applying program synthesis techniques for generating visualisations! Elegant and practical.
Highlight of #POPL yesterday: seeing some excellent discussions of Coq for verifying programming languages!
https://popl20.sigplan.org/details/PLMW-POPL-2020/3/Theorem-provers-are-a-P-L-researcher-s-best-friend
I came away with a much clearer sense of *how* you'd verify an optimising compiler.
One wonderful aspect of POPL is being able to speak to experts.
I've admired Nadia Polikarpova's synthesis work for a while, so I jumped at the opportunity to do a Synquid tutorial led by her!
Invited talk: Safety Verification for Deep Neural Networks: https://popl20.sigplan.org/details/VMCAI-2020-papers/22/Safety-and-Robustness-for-Deep-Learning-with-Provable-Guarantees
How do we verify that a DNN is robust to adversarial attacks? How do we quantify safety? This approach looks at image features (Sift) and verifies all perturbations within a region.
Day 1 at @poplconf had a bunch of interesting talks at VMCAI (Verification, Model Checking, and Abstract Interpretation). https://popl20.sigplan.org/home/VMCAI-2020
Thread.
Handy project that gives GitHub buttons tracking release versions across different Linux distros:
You can even get smart Rubik's Cubes now! It pairs with bluetooth, and of course there's a corresponding app that gives you feedback.
https://youtu.be/ez8x5JDLexU?t=390
What other toys could we add computers to?
It's hard to get developers to pay for tools. I think the problem is that computers are incredibly general machines.
Once you've worked in programming for a while, it's easy to imagine making a whole range of tools. It's hard to guess the complexity of new domains though.
Lovely example of transpiling C to brainfsck, including a discussion of parsing, handling variables, assignments, and even function calls!
https://www.bozidarevic.com/2019/12/transpiling-c-into-brainfuck/
One interesting consequence of home automation devices is it enables presence when you're not at home.
You can switch on lights or even talk through a smart doorbell. Will this change expectations of visitors?
Finally migrated my 2014-era web application off an old server.
When I set it up, I tried to take good notes. These days I expect a bundle I can deploy with command -- a list of required packages is distro-specific, labour intensive, and bitrots!
Interesting that some web hosts see the least traffic over Christmas! https://blog.nearlyfreespeech.net/2019/12/24/maintenance-for-christmas/
Showing 346-360 of 378 posts