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

Ubuntu Emailing With Thunderbird And Android's K-9

Continuing email beginner's guide, now we Ubuntu users who have Android can read our emails anywhere anytime in both devices. It's a wonderful experience. On computer we use Thunderbird, while on phone we use K-9, both are free software. This tutorial uses Disroot email account as example, thanks to its gratis IMAP feature. Now, let's go! Fortunately, Ubuntu users do not need to install anything anymore. But for Android users, you will install K-9 Email Client, it is available at free software center F-Droid. Read more

Write GIMP scripts to make image processing faster

Some time ago, I wanted to give a blackboard-style look to a typeset equation. I started playing around with the GNU Image Manipulation Program (GIMP) and was satisfied with the result. The problem was that I had to perform several actions on the image, I wanted to use this style again, and I did not want to repeat the steps for all the images. Besides, I was sure that I would forget them in no time. GIMP is a great open source image editor. Although I have been using it for years, I had never investigated its batch-processing abilities nor its Script-Fu menu. This was the perfect chance to explore them. Read more

Use your Raspberry Pi as a productivity powerhouse

In prior years, this annual series covered individual apps. This year, we are looking at all-in-one solutions in addition to strategies to help in 2021. Welcome to day 16 of 21 Days of Productivity in 2021. The Raspberry Pi is a pretty amazing little computer—small, surprisingly powerful, and very easy to set up and use. I have used them for home automation projects, dashboards, and a dedicated media player. But can it be a productivity powerhouse as well? The answer is, quite simply, yes. Read more

Mozilla Firefox 85.0 Now Available As First 2021 Release

Mozilla Firefox 85.0 is available today as the open-source web browser's first major release of the year. For those more interested in Firefox now following the recent news of Google cutting off Chromium API access to various Google services in trying to steer more users to Chrome proper, Firefox 85.0 has arrived just in time. Firefox 85.0 is available this morning via the Mozilla FTP ahead of the official announcement. Firefox 85.0 comes with privacy enhancements like network partitioning, the password manager can now more easily remove all saved logins, and the Adobe Flash support is removed in full. Read more