Language Selection

English French German Italian Portuguese Spanish

Mozilla on Synthesizing Loop-Free Programs with Rust and Z3 and on Privacy

Filed under
Development
Moz/FF
  • Synthesizing Loop-Free Programs with Rust and Z3

    Automatically finding a program that implements a given specification is called program synthesis. The main difficulty is that the search space is huge: the number of programs of size \(n\) grows exponentially. Naïvely enumerating every program of size \(n\), checking whether each one satisfies the specification, and then moving on to programs of size \(n+1\) and so on doesn’t scale. However, the field has advanced by using smarter search techniques to prune the search space, leveraging performance improvements in SMT solvers, and at times limiting the scope of the problem.

    In this post, I’ll explain one approach to modern program synthesis: counterexample-guided iterative synthesis of component-based, loop-free programs, as described in Synthesis of Loop-Free Programs by Gulwani et al. We’ll dissect exactly what each of those terms mean, and we’ll also walk through an implementation written in Rust that uses the Z3 solver.

  • No judgment digital definitions: Online advertising strategies

    It’s hard to go anywhere on the internet without seeing an ad. That’s because advertising is the predominant business model of the internet today. Websites and apps you visit every day are largely “free” for you because they monetize your data and your attention through advertising. And, as data sets of individuals and groups online have become more readily available to companies in recent years, advertisers have developed strategies to minimize what they spend on ads while maximizing the profit made from them. The ad tech arms race is constantly evolving, and the more invasive practices that are used, the more valuable your data is. Here are some of the most common online advertising strategies and associated activities being used that rely on collecting data about you today.

More in Tux Machines

today's howtos

Devices/Embedded With GNU/Linux

Easy Librem 5 App Development: Flashlight

In my first post on easy application development on the Librem 5 I discussed how to turn a simple shell script that takes a screenshot into a full graphical app with only a few extra lines of code. In this post I will follow up with an even simpler application that took about twenty minutes to write with much of that time involved in reading documentation. My Bright Idea The interesting thing about smart phones is how many other devices they have replaced beyond a regular phone. For instance, there used to be a market for small, pocket-sized digital cameras, but now many people just use the cameras on their smart phones. While some people still do keep a pocket flashlight with them, many people just use the light on their smart phone. I realized that a flashlight app would be another great way to showcase just how easy it is to develop applications for the Librem 5. As applications go the requirements are pretty simple: you need a button to turn on the light, a button to turn off the light, and a button to close the app. Read more

LibreOffice Writer Articles and Improvements

  • Two alternatives to Microsoft Word that are free and customizable

    If you're looking for an open-source office suite, LibreOffice is the software package for you. Its word processing program is LibreOffice Writer--which, incidentally, this story was written with, so I can attest to its excellence. You're able to choose from different fonts and text styles, embed images and figures, and use a variety of other functions you'd expect from its paid competition. It can save files in an Open Document Format (ODF), a number of Word formats, and export your work as a PDF for wide-ranging compatibility.

  • Improved rotated text handling in Writer's table rows with automatic height

    Writer now has better support for rotated text in tables containing rows with automatic height. This post also presents two related fixes. First, thanks Otevřená města who made this work by Collabora possible. [...] Before diving into improved rotated text handling, first a continuous section break import problem (tdf#128605) was fixed: this was a case when we created a new page style, but only a new section was intended.