Skip to content

Instantly share code, notes, and snippets.

@jberthold

jberthold/Day-2.md

Last active January 25, 2023 04:13
Show Gist options
  • Save jberthold/35a8a7aa51d1964ec70a47a1a3f94a92 to your computer and use it in GitHub Desktop.
Save jberthold/35a8a7aa51d1964ec70a47a1a3f94a92 to your computer and use it in GitHub Desktop.
Download ZIP
Splash Day 2 Notes
Raw
Day-2.md

Notes at SPLASH 2022 - 20221205-10 Auckland NZ

Tue 6 12 - Keynote day

Unsound Workshop: Keynote

About the workshop

new workshop. Motivation: verification systems became so popular but also so complex that proving the tools themselves becomes too hard.

  • compromises made for ease of use and presentation
  • theoretical background varies depending on the approach
    • hard to understand and distinguish the particular details of key definitions, such as "unsound"
  • goal: establish a forum for dialogue between different research lines and sharing of potential pitfalls and limitations
  • "publishing negative results" to build a corpus of experience reports
  • particular interest: wrong assumptions shared by several approaches ("broken foundations")

Keynote: Jan Bessai, "What do we mean by 'Unsound`"

(virtual)

  • First insight: Unsoundness of a system (violation of its contract) could occur because of tool deficiencies (false negative) or because the system used to specify the contract itself is deficient.

  • Flavours of unsoundness in classical logic

    • inconsistent logic (deriving false from empty, ∅ ⇒ ⊥
    • ex-falso (prove what you want from false) and weakening (dropping preconditions) together prove everything
    • some systems include one or the other, but can sustain it because the respective other one is missing

  • Semantic deficiency:

    • unsound interpretation (where properties get lost in interpretation)
    • in particular, violated equation interpretatoin (see screenshot), turning interpreted functions into relations

  • Unsound models:

    • A model is unsound if it does not (fully) describe behaviours of the modelled system. Example: pointers and fields (structs) with overlap (reference assumes non-overlap), or totality for OO languages

  • About theorem provers:

    • famous deficiencies and bugs in theorem provers were found in the past, and will be discovered in the future
      • Girard's paradox (type of a type is "type"), Univalence + UIP (uniqueness of identity) in Agda, Famous Coq bug
    • inherent problem becomes worse with proof system modularity: combining silently inconsistent libraries (which are consistent in and of themselves)
    • interesting data point: Idris accepts and includes type-in-type, and states it as a warning in the release notes.

  • different classes of problems

    • checker bug: can be fixed easily
    • inconsistent logic: can be restricted, may be fixed
    • unsound model: systematic problem, needs paradigm shift

  • other topics/issues to discuss in the new workshop:

    • subject reduction bugs: reduction of a program changes types (happens today in Java, class cast)
    • models of resources (hardware limitations and potential errors neglected, unrealistic cost models like O(1) for bignum)
    • ignoring deployment/environment issues
    • social issues:
      • scientific community and industry have unhelpful incentive structures, individuals have hidden agendas

LIVE Workshop: Keynote

Peter van Hardenberg: "Searching for Life"

  • intro: motivating "dynamic distraction-free working tools, making computers companions/tools for our thinking"

  • requirements: reliability, immediacy, "becoming invisble"

    • also: portability, independence of environment, ease of use, privacy and collaboration

  • Talk topic: the appeal of live coding performance (music)

    • also present in captures of video game walk-throughs etc. (particular games, collaborative Virtual World creation)

  • "Live programming"

    • examples: SQL DB interaction, bash scripting, spreadsheets, ..
    • unlike enterprise software!

  • keeping programming alive:

    • matter of size (think DB tuple counts), and program size and complexity
    • trade-off of liveliness vs. stability, risk appetite of changes

  • Research at "Ink & Switch"

    • "Programmable Ink", sketch-book suporting dynamic scripting to animate notes (with a drwwing interface), "Untangle" graphical interface to an SMT solver (in a dialogue with the machine)

      • goal: natively programming by sketches (not an isomorphism to something textual and known)
      • interesting datapoints: visual programming never produces invalid programs
      • the challenge of scalability remains (like node-and-wire programs) - addressed "in a separate set of tools"

    • Malleable software (-> Philip Tchernavskij), erasing boundaries between different apps and tools.

    • "Local-first software": (not google docs, not github, but a middle ground)

      • killer app: journalistic collaboration, where accuracy and speed equally matter.
        • NYT had a google doc app with additional procedural views and meta-information. Network is crucial (big drawback), reliability even more.
      • contrast with github: async, PR process, non-collaboration
        • or rather this is about the latency differences, the essential issues are the same but the perception is vastly different.
      • Ideas and goals:
        • live building and collaboration
        • versus deliberate controlled sharing and distribution
        • Core principle: Never stop the user from making progress.
          • accepting the risk of breakage for the sake of potential progress

  • personal thought:

    • combining these ideas with the haptic experience of a smart board or multi-touch screen table. How to paradigms and goals change? (probably a triviality in the HCI community, though)

  • concluding thought:

    • zombie programs start as small living things. Keep things strategically small.

  • Questions:

    • Role of AI
      • great collaborator but poor tool
    • ..(missed)..
      • we are locked up in the 1970's notion of plain text and posix FS
    • HW desirables
      • Ipad not great. Remarkable, stylus, .. . Cloud will never be fast, you have 10ms for the "local" look+feel
    • Do we need new PLs to develop the new tools you envision?
      • "An empirical question" - just like we need many different tools to be efficient in a wood workshop, it will have diverse answers.

Potluck, dynamic doc.s as personal software

(Random talk following the keynote)

  • observation: note-taking apps insufficient in functionality, many apps (like recipe apps) have fixed rigid schema, and always focus on particular domains
  • "gradual enrichment" of plain notes with functionality over time, adding dynamic functionality, in an iterative process

GPCE: Keynote

Generative Programming, Concepts and Experiences

Keynote: David Pearce (Consensys), Lang. design meets verifying compilers

  • "verifying compilers"

Problem space

  • (how) are things changing in the world of programming?
    • (showing old code from 1995, which would be written the same way today)
  • early ideas on program checking/verification
    • decomposition into smaller properties etc.
    • recognised as a fundamental activity in the very early days (Turing)
  • 1979 earliest "verifying compiler": Stanford Pascal Verifier
  • 2003: Tony Hoare setting out verifying compilers as a grand challenge
  • today, "almost there". Verifying compilers not mainstream but special tools being used in industry by practicioners
    • BUT: Eth deposit contract, with an infamous "this should be impossible" statement. No formal proof of that guarantee.

Setting

  • Dafny compiler to model and verify solidity code
  • 2 languages: Dafny (of MSR, now AWS), Whiley (of his own making)
    • lending themselves to verification
    • initially compiling to boogey and using z3 to verify
    • featuring ensures on functions/routines

Verifying compilers

  • mere translation is not the main purpose of a "compiler" any more today

    • loads of checks are performed
    • true verifying compilers especially
    • (NB and the target language is (in one way or another) source again more often than not)

  • a verifying compiler pipeline: where is the verification?

    • option 1: replace type-check and other static analysis by "verification" stage
      • assumes verifier is smarter, can accept more good programs (??)
      • drawbacks: performance of the verification, no time bounds
      • (Claim: verifiers are still immature)
    • option 2:
      • verification follows on from typing and other analyses

  • code example: assumptions stated allow one to write "unsafe" code, different from what would be written without it.

    • whiley program does not type-check, never reaches the verifier. -> language design aspect
    • Whiley allows for an assertion to convince the type checker
    • similar example: missing return statement on fully-covering if cascade. Dafny can infer this, Whiley cannot (needs to use fail).

Aspects: Flow typing functional purity, uninterpreted functions, inference

  • "types are influenced by positions in the control flow"

    • example: index-of returning an option that is present

  • purity: not present as a language concept in any imperative language

  • latest approaches: purity established, capitalise on static (use) analysis to mutate data partially instead of a copy. This is an optimisation. Recursion (required in Dafny) would hide such a partial update

  • uninterpreted functions:

    • essential tool for Dafny-based verification: marking functions as "uninterpreted" (opaque) => work exclusively from its specification
    • Dafny proofs involving "method" require stating all required properties for a proof (nethods are opaque), functions are accessible
      • Whiley has the interpreted function and the uninterpreted property
      • function can be annotated "uninterpreted"

  • Inference

    • example (index-of with precondition) shows why function/method is useful.

    • invariant in the loop ensures final assert(false) unreachable

    • OTOH the array index-in-bounds definedness is not automatic in Dafny (but in Whiley)

  • Questions:

    • What are the trade-offs helping to decide what design is better?
      • "if z3 works, don't do it as in Whiley, do it like Dafny"
    • trade-off between unbounded integers and implementation
    • Are we making the compiler too smart? We want to understand it!
      • example of the Rust borrow-checker.. difficult!
      • smartness can help, e.g. giving counterexamples
    • From implementation experience, what is annoying in Whiley/Dafny?
      • definedness inference by inferred preconditions (Whiley)
      • functions do not compile to code (Dafny), needs special annotation. Rutime checks must be possible

TODO Conversation with Bernhard Scholz (UoSydney, Fantom)

  • reaching out actively to get in touch about collaborations
  • TODO reach out to Everett (and Grigore?), follow up

Unsound: "The four horsemen of unsoundness in OO languages"

(joined towards the end)

  • Positivity checker (in Coq and in usual OO idioms)
    • "[either] you can prove false [or...] you just don't have OO"

  • Questions:
    • What do you mean by "OO"? code reuse vs. use of contracts
      • leading to a philosophical discussion about the goals, probably also a dispute about community beliefs.
  • Workshop steering discussion

GPCE papers session

LINQ for temporal data

  • temporal data in SQL11 standard, but rarely implemented
  • this work: proposing LINQ support
  • key point: data never lost, instead it is replicated with a timestamp reflecting state change
  • valid time vs transaction time
    • transaction time is the above. valid time is user-defined
    • current state of implementation: one or the other
  • different kinds of updates, including time-windowed (sequenced)

  • key idea of the integration:
    • translate temporal statements into non-temporal lower level

Type System for four delimited control opreators

(best paper award)

  • applying types to "delimited control" opreators
    • control flow operators that exist in pairs (capturer, delimiter)
    • capturers differ, delimiters are mere parentheses
  • proposing a type system that unifies four different (existing) delimited control opreators, retaining prior theoretical work and comparing all four

  • builds on a corpus of earlier work using CPS interpreters
    • completing the picture of the four control operators wrt.types

SQL to Stream with S2S (tool paper)

  • compiling SQL to Java Stream API

    • pipeline of operations (create, mapping/filtering, aggregation)
    • API often imposes a considerable performance penalty
      • lack of benchmarks, optimisation work ongoing but limited
    • idea: use conversion to create benchmarks

  • approach: compile query plans to java using stream API

    • QUESTION: is it always straightforward to transform to stream-java?

  • problems with aggregation (when multiple aggreg. functions)

    • compile into a custom aggregation function
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment