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

Python Programming Leftovers

  • The tiniest of Python templating engines

    In someone else's project (which they'll doubtless tell you about themselves when it?s done) I needed a tiny Python templating engine. That is: I wanted to be able to say, here is a template string, please substitute a bunch of variables into it. Now, Python already does this, in about thirty different ways, and str.format or string.Template do most of it as built-in.

  • How to set a variable in Django template
  • Why ASGI is Replacing WSGI in Django

    When I first learnt about how to deploy my Django website. I took the easy route which was deploying it on Heroku. There's literally tons of tutorial on how the process of deploying it work. Heck, there was even a book about the benefits of deploying Django using Heroku. Soon in my own work, I needed to deploy my own Django project. It was working well for a bundled development grade web server. I thought to myself, why not find a better way on a production-grade web server. Instead of just a miserable default web server that is not production-grade. My journey in searching on deploying Django started for me. Which if you look at multiple tutorial references they still suggest the use of Heroku or Digital Ocean.

  • Weekly Python StackOverflow Report: (ccxi) stackoverflow python report
  • Understand predicate pushdown on row group level in Parquet with pyarrow and python

    We are using the NY Taxi Dataset throughout this blog post because it is a real world dataset, has a reasonable size and some nice properties like different datatypes and includes some messy data (like all real world data engineering problems).

Android Leftovers

MNT Reform 2 Open Source DIY Arm Linux Modular Laptop Coming Soon (Crowdfunding)

We first covered MNT Reform in fall of 2017, when it was a prototype for a DIY and modular laptop powered by NXP i.MX 6QuadPlus processor, and with plans to eventually use i.MX 8 hexa-core processor. Last year they designed several beta units of Reform to get feedback for a dozen users, and have now fully redesigned the laptop based on an NXP i.MX 8M system-on-module with the crowdfunding campaign expected to go live in February on Crowd Supply. The goals of the project are to provide an open-source hardware laptop that avoids binary blobs as much as possible and is environmentally friendly. These goals guided many of the technical decisions. For example, there are many NXP i.MX 8M SoM’s, but MNT selected Nitrogen8M as the schematics are available after registration on Boundary Devices website, and that means people wanting to create their own module compatible with Reform 2 could do so. Read more

today's leftovers and howtos

  • [Ubuntu] Design and Web team summary – 17 January 2020

    The second iteration of this year is the last one before our mid-cycle sprint next week. Here’s a short summary of the work the squads in the Web & Design team completed in the last 2-week iteration.

  • 5 key steps to take your IoT device to market

    IoT businesses are notoriously difficult to get off the ground. No matter how good your product is or how good your team is, some of the biggest problems you will face are just in getting to market and maintaining your devices once they’re in the field. The webinar will take a look at how Canonical’s Brand Store product allows you to get to market while catering for long term problems and the need to keep your product up to date in the future. More specifically, this webinar will look at the common problems we see organisations facing on their way to getting an IoT device to market, and cover five key steps to solve these problems. Along the way we will dig a little into serval case studies Canonical has done with various customers and partners to show you what has already been achieved with these solutions.

  • Fake cases — make sure yours is the real deal

    We’ve had some reports of people finding cases that pretend to be official Raspberry Pi products online — these are fakes, they’re violating our trademark, they’re not made very well, and they’re costing you and us money that would otherwise go to fund the Raspberry Pi Foundation’s charitable work. (Reminder, for those who are new to this stuff: we’re a not-for-profit, which means that every penny we makes goes to support our work in education, and that none of us gets to own a yacht.)

  • Let’s Talk With Neal Gompa of Fedora @ openSUSE Conference

    In this episode of Let’s Talk, we sat down with Neal Gompa of the Fedora community at openSUSE Conference

  • FOSSCOMM 2019 aftermath

    FOSSCOMM (Free and Open Source Software Communities Meeting) is a Greek conference aiming at free-software and open-source enthusiasts, developers, and communities. This year was held at Lamia from October 11 to October 13. It is a tradition for me to attend this conference. Usually, I have presentations and of course, booths to inform the attendees about the projects I represent. This year the structure of the conference was kind of different. Usually, the conference starts on Friday with a "beer event". Now it started with registration and a presentation. Personally, I made my plan to leave Thessaloniki by bus. It took me about 4 hours on the road. So when I arrived, I went to my hotel and then waited for Pantelis to go to University and set up our booths.

  • Fugue open sources Regula to evaluate Terraform for security misconfigurations and compliance violations

    Regula rules are written in Rego, the open source policy language employed by the Open Policy Agent project and can be integrated into CI/CD pipelines to prevent cloud infrastructure deployments that may violate security and compliance best practices. “Developers design, build, and modify their own cloud infrastructure environments, and they increasingly own the security and compliance of that infrastructure,” said Josh Stella, co-founder and CTO of Fugue. “Fugue builds solutions that empower engineers operating in secure and regulated cloud environments, and Regula quickly and easily checks that their Terraform scripts don’t violate policy—before they deploy infrastructure.”

  • Finance goes agile as open source checks the security box

    “At Northwestern Mutual, we’ve finally gotten past that curve,” said Sean Corkum (pictured, right), senior engineer at Northwestern Mutual. “Now we’re trying to make it even easier for our internal developers to participate in open source … and contribute more to the community.”

  • Top NLP Open Source Projects For Developers In 2020
  • Kiwi TCMS: Project roadmap 2020

    Hello testers, the Kiwi TCMS team sat down together last week and talked about what we feel is important for us during the upcoming year. This blog post outlines our roadmap for 2020!

  • Shift on Stack: api_port failure
  • How To Git Commit With Message