https://blog.brownplt.org/2024/04/21/forge.html

The Brown PLT Blog

[brownplt]

RSS

CONTACT

GROUP PAGE

PREVIOUS POSTS

  * Forge: A Tool to Teach Formal Methods
  * Finding and Fixing Standard Misconceptions About Program Behavior
  * Privacy-Respecting Type Error Telemetry at Scale
  * Profiling Programming Language Learning
  * The Examplar Project: A Summary
  * A Core Calculus for Documents
  * Observations on the Design of Program Planning Notations for
    Students
  * Conceptual Mutation Testing
  * Generating Programs Trivially: Student Use of Large Language
    Models
  * A Grounded Conceptual Model for Ownership Types in Rust
  * What Happens When Students Switch (Functional) Languages
  * Typed-Untyped Interactions: A Comparative Analysis
  * Little Tricky Logics
  * Identifying Problem Misconceptions
  * Performance Preconceptions
  * Structural Versus Pipeline Composition of Higher-Order Functions
  * Plan Composition Using Higher-Order Functions
  * Towards a Notional Machine for Runtime Stacks and Scope
  * Gradual Soundness: Lessons from Static Python
  * Applying Cognitive Principles to Model-Finding Output
  * Automated, Targeted Testing of Property-Based Testing Predicates
  * A Benchmark for Tabular Types
  * Student Help-Seeking for (Un)Specified Behaviors
  * Adding Function Transformers to CODAP
  * Developing Behavioral Concepts of Higher-Order Functions
  * Adversarial Thinking Early in Post-Secondary Education
  * Teaching and Assessing Property-Based Testing
  * Students Testing Without Coercion
  * Using Design Alternatives to Learn About Data Organizations
  * What Help Do Students Seek in TA Office Hours?
  * Combating Misconceptions by Encouraging Example-Writing
  * The Hidden Perils of Automated Assessment
  * Mystery Languages
  * Resugaring Type Rules
  * Picking Colors for Pyret Error Messages
  * Can We Crowdsource Language Design?
  * Crowdsourcing User Studies for Formal Methods
  * User Studies of Principled Model Finder Output
  * A Third Perspective on Hygiene
  * Scope Inference, a.k.a. Resugaring Scope Rules
  * The PerMission Store
  * Examining the Privacy Decisions Facing Users
  * The Pyret Programming Language: Why Pyret?
  * Resugaring Evaluation Sequences
  * Slimming Languages by Reducing Sugar
  * In-flow Peer Review: An Overview
  * Tierless Programming for SDNs: Differential Analysis
  * Tierless Programming for SDNs: Verification
  * Tierless Programming for SDNs: Optimality
  * Tierless Programming for SDNs: Events
  * Tierless Programming for Software-Defined Networks
  * CS Student Work/Sleep Habits Revealed As Possibly Dangerously
    Normal
  * Parley: User Studies for Syntax Design
  * Typechecking Uses of the jQuery Language
  * Verifying Extensions' Compliance with Firefox's Private Browsing
    Mode
  * From MOOC Students to Researchers
  * Social Ratings of Application Permissions (Part 4: The Goal)
  * Social Ratings of Application Permissions (Part 3: Permissions
    Within a Domain)
  * Social Ratings of Application Permissions (Part 2: The Effect of
    Branding)
  * Social Ratings of Application Permissions (Part 1: Some Basic
    Conditions)
  * Aluminum: Principled Scenario Exploration Through Minimality
  * A Privacy-Affecting Change in Firefox 20
  * The New MOOR's Law
  * Essentials of Garbage Collection
  * (Sub)Typing First Class Field Names
  * Typing First Class Field Names
  * S5: Engineering Eval
  * Progressive Types
  * Modeling DOM Events
  * Mechanized LambdaJS
  * ECMA Announces Official lJS Adoption
  * Objects in Scripting Languages
  * S5: Wat?
  * Belay Lessons: Smarter Web Programming
  * S5: Semantics for Accessors
  * S5: A Semantics for Today's JavaScript
  * The Essence of JavaScript
  * ADsafety

Forge: A Tool to Teach Formal Methods

Posted on 21 April 2024.

For the past decade we have been studying how best to get students
into formal methods (FM). Our focus is not on the 10% or so of
students who will automatically gravitate towards it, but on the
"other 90%" who don't view it as a fundamental part of their
existence (or of the universe). In particular, we decided to infuse
FM thinking into the students who go off to build systems. Hence the
course, Logic for Systems.

The bulk of the course focuses on solver-based formal methods. In
particular, we began by using Alloy. Alloy comes with numerous
benefits: it feels like a programming language, it can "Run" code
like an IDE, it can be used for both verification and
state-exploration, it comes with a nice visualizer, and it allows
lightweight exploration with gradual refinement.

Unfortunately, over the years we have also run into various issues
with Alloy, a full catalog of which is in the paper. In response, we
have built a new FM tool called Forge. Forge is distinguished by the
following three features:

 1. Rather than plunging students into the full complexity of Alloy's
    language, we instead layer it into a series of language levels.

 2. We use the Sterling visualizer by default, which you can think of
    as a better version of Alloy's visualizer. But there's much more!
    Sterling allows you to craft custom visualizations. We use this
    to create domain-specific visualizations. As we show in the
    paper, the default visualization can produce unhelpful,
    confusing, or even outright misleading images. Custom
    visualization takes care of these.

 3. In the past, we have explored property-based testing as a way to
    get students on the road from programming to FM. In turn, we are
    asking the question, "What does testing look like in this FM
    setting?" Forge provides preliminary answers, with more to come.

Just to whet your appetite, here is an example of what a default
Sterling output looks like (Alloy's visualizer would produce
something similar, with fewer distinct colors, making it arguably
even harder to see):

Default Sterling output

Here's what custom visualization shows:

Custom Sterling output

See the difference?

For more details, see the paper. And please try out Forge!