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! https://popl20.sigplan.org/details/POPL-2020-Research-Papers/31/Augmented-Example-based-Synthesis-using-Relational-Perturbation-Properties
miniblog.
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. https://popl20.sigplan.org/details/POPL-2020-Research-Papers/53/Visualization-by-Example
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!
https://popl20.sigplan.org/details/POPL-2020-tutorialfest/3/-T3-Synthesizing-Programs-from-Types
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: https://repology.org/
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/
You can now buy lamps with speakers you can control remotely: https://www.ikea.com/gb/en/p/symfonisk-table-lamp-with-wifi-speaker-black-50357592/
I imagine we'll see home devices integrating smart speakers rather than separate devices eventually.
Perhaps all links should have a tooltip with a preview of the content. I'm struggling to see a downside.
We moved from double- to single-clicking links, why not make the site/browser do more work before clicking?
I'll be at @poplconf 2020! Do say hello.
Cute elisp trick I haven't seen before: point works as a place with setf!
;; Move point to the beginning of the buffer
(setf (point) (point-min))
;; Equivalent:
(goto-char (point-min))
I still find it amazing that Google provides _free_, _unlimited_ image storage at a reasonable resolution.
It's a really nice service, but I don't understand the economic rationale.
GitHub now provides a feature to discover when you've accidentally leaked company private keys: https://developer.github.com/partnerships/token-scanning/
Makes sense, but it's a shame it's needed. It's easy to screw up.
Showing 1,561-1,580 of 7,508 posts