• Into the Well of Formal Verifications

  • 2024/11/20
  • 再生時間: 59 分
  • ポッドキャスト

Into the Well of Formal Verifications

  • サマリー

  • This week Mike and Erik were trying to understand the arena of formal verification: what are these tools? Where do they come from? How do they work? Can we categorize them?

    There's a ton of stuff to talk about in this area and we're just learning the things, so we made an attempt here to wade in and figure stuff out!

    We also mentioned on this episode that there are some new ways to reach out to us (in addition to our email address), but they are:

    - Bluesky account: https://bsky.app/profile/picturemecoding.bsky.social
    - Threadless store (in case you want a Picture Me Coding coffee mug or stickers!): https://picturemecoding.threadless.com/
    - Existing email address: podcast@picturemecoding.com

    Here Are Some Links to Stuff We Discussed

    • Lamport’s A Science of Concurrent Programs (pdf)
    • Dafny
    • Cloudflare’s Formally Verified DNS
    • P language
    • Wadler’s Propositions as Types paper
    • Hillel Wayne’s “Let’s Prove Leftpad” and repo
    • Amazon Science page on “automated reasoning” as an area
    • Amazon paper “Model checking distributed protocols in Must”

    Send us a text

    続きを読む 一部表示

あらすじ・解説

This week Mike and Erik were trying to understand the arena of formal verification: what are these tools? Where do they come from? How do they work? Can we categorize them?

There's a ton of stuff to talk about in this area and we're just learning the things, so we made an attempt here to wade in and figure stuff out!

We also mentioned on this episode that there are some new ways to reach out to us (in addition to our email address), but they are:

- Bluesky account: https://bsky.app/profile/picturemecoding.bsky.social
- Threadless store (in case you want a Picture Me Coding coffee mug or stickers!): https://picturemecoding.threadless.com/
- Existing email address: podcast@picturemecoding.com

Here Are Some Links to Stuff We Discussed

  • Lamport’s A Science of Concurrent Programs (pdf)
  • Dafny
  • Cloudflare’s Formally Verified DNS
  • P language
  • Wadler’s Propositions as Types paper
  • Hillel Wayne’s “Let’s Prove Leftpad” and repo
  • Amazon Science page on “automated reasoning” as an area
  • Amazon paper “Model checking distributed protocols in Must”

Send us a text

Into the Well of Formal Verificationsに寄せられたリスナーの声

カスタマーレビュー:以下のタブを選択することで、他のサイトのレビューをご覧になれます。