5 ms·

Reasoning About Program Behavior Algebraically [pdf]

113 points by rwosync 9y ago

alfonsodev 9y ago
Very interesting, What is the programming language used in the code examples ?
- Ezku 9y ago
  That's Haskell. Slides 4 & 5 also hint at that, although it's easy to miss: > Why Haskell is Interesting
  - empath75 9y ago
    Even if you never intend to use Haskell it’s well worth getting a basic understanding of it if you have an interest in CS theory just because it’s used so frequently in interesting talks and papers.
Rainymood 9y ago
Sorry for being off-topic, but those slides are beautiful. Does anyone know what they're made in?
- Luc 9y ago
  Google Slides.
neoberg 9y ago
Is the talk recorded? Can we find it somewhere?
- tome 9y ago
  Functional Works "might release the talks soon". https://www.reddit.com/r/haskell/comments/7l2z7d/pdf_stephen_diehl_reasoning_about_program/drk9y2c/ https://www.reddit.com/r/haskell/comments/7l2z7d/pdf_stephen...
mrkgnao 9y ago
From experience (the last time slides for a talk by Stephen Diehl made its way to the HN frontpage), there's a lot of information in the actual (recorded) talk that the slides are going to be missing.
- msangi 9y ago
  Is the video available?
yawaramin 9y ago
There are a lot of advanced techniques in these slides, but if you care about program behaviour, in a functional context that mostly reduces to caring about the types of your functions. E.g., in Haskell if you have a function of type `a -> a` you know that it must be the identity function (leaving aside exceptions and undefined). Taking this further, you can define functions of types that specify your desired behaviour exactly, e.g. guess what this does: foo :: List a -> SortedList a Or this: bar :: VerificationToken -> Email Unverified -> Email Verified That's really the main idea. If you specify the types in the right way, you can make them describe the function quite nicely.
- cmrx64 9y ago
  People like to tout this idea about a lot, but I've never seen it used in any rigorous way. It's SUGGESTIVE of program behavior, but I haven't seen any tools for (attempted) extraction of even just FSMs from basic type-level state machines like that. You want to write down a property about "Email Verified" and the paths to values of that type and have the system check it. Real programs are too large for mere suggestion to have any assurance value. ... and I think this presentation had a lot more to offer than the absolute bog-standard techniques of labeled transition systems, whether you do it in the types or not.
  - yawaramin 9y ago
    I don't understand your points, I guess. Your first point is that you've never seen this technique used in any rigorous way, and your second point is that it's an absolute bog-standard technique? I don't follow.

113 points by rwosync 9y ago

alfonsodev 9y ago

Very interesting, What is the programming language used in the code examples ?

Ezku 9y ago
That's Haskell. Slides 4 & 5 also hint at that, although it's easy to miss: > Why Haskell is Interesting
- empath75 9y ago
  Even if you never intend to use Haskell it’s well worth getting a basic understanding of it if you have an interest in CS theory just because it’s used so frequently in interesting talks and papers.

Rainymood 9y ago

Sorry for being off-topic, but those slides are beautiful. Does anyone know what they're made in?

Luc 9y ago
Google Slides.

neoberg 9y ago

Is the talk recorded? Can we find it somewhere?

tome 9y ago
Functional Works "might release the talks soon". https://www.reddit.com/r/haskell/comments/7l2z7d/pdf_stephen_diehl_reasoning_about_program/drk9y2c/ https://www.reddit.com/r/haskell/comments/7l2z7d/pdf_stephen...

mrkgnao 9y ago

From experience (the last time slides for a talk by Stephen Diehl made its way to the HN frontpage), there's a lot of information in the actual (recorded) talk that the slides are going to be missing.

msangi 9y ago
Is the video available?

yawaramin 9y ago

There are a lot of advanced techniques in these slides, but if you care about program behaviour, in a functional context that mostly reduces to caring about the types of your functions. E.g., in Haskell if you have a function of type `a -> a` you know that it must be the identity function (leaving aside exceptions and undefined). Taking this further, you can define functions of types that specify your desired behaviour exactly, e.g. guess what this does: foo :: List a -> SortedList a Or this: bar :: VerificationToken -> Email Unverified -> Email Verified That's really the main idea. If you specify the types in the right way, you can make them describe the function quite nicely.

cmrx64 9y ago
People like to tout this idea about a lot, but I've never seen it used in any rigorous way. It's SUGGESTIVE of program behavior, but I haven't seen any tools for (attempted) extraction of even just FSMs from basic type-level state machines like that. You want to write down a property about "Email Verified" and the paths to values of that type and have the system check it. Real programs are too large for mere suggestion to have any assurance value. ... and I think this presentation had a lot more to offer than the absolute bog-standard techniques of labeled transition systems, whether you do it in the types or not.
- yawaramin 9y ago
  I don't understand your points, I guess. Your first point is that you've never seen this technique used in any rigorous way, and your second point is that it's an absolute bog-standard technique? I don't follow.