PNW PLSE Workshop 2023 Observations and Gained Insights

10:30 - Talks

Linear Types for Systems Verification

It is a good idea to embed verification information in type system of a programming language.

Verified Program Construction

• Program verification is hard per se.
  • Proofs are brittle.
  • Existing techniques provide poor support for commonly-used datatypes such as vectors, sets, and maps.
  • Partial verification is important due to the complexity of programs.
• Program verification for general-purpose programming languages and frameworks for general-purpose programming languages is tedious compared to focusing on a DSL.
• The direction for program verification should be verified program construction.
• Be aware of the pain point you are trying to solve and the day-to-day engineering reality in real-world software development.

13:00 - Keynote: Patrick Lam

Hot Takes on Machine Learning for Program Analysis

• A crucial step in Machine Learning for Program Analysis is deciding what things could be used as features based on experience.
• Generative AI can replace junior developers doing raw coding instead of contextual work.

13:30 - Lightning Talks

Lakeroad: Hardware Compilation via Program Synthesis

If you don't use DSLs, FPGAs bring crappy performance running programs in general-purpose programming languages.

Checked C

Retrofitting verification into non-verified languages is an arduous task.

15:15 - Talks

An Anti-Capitalist, Multicultural, Accessible Programming Language

An event-based language enabling time-traveling to all points in program execution history would greatly benefit debugging.