Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Reasoning About Program Behavior Algebraically [pdf]

dev.stephendiehl.com

Post reply on HN
Print view View original

11–13 of 13 posts

Re: Reasoning About Program Behavior Algebraically [pdf]

#11

Post by yawaramin »

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.

Re: Reasoning About Program Behavior Algebraically [pdf]

#12

Post by cmrx64 »

yawaramin wrote: post #11

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 behavio…

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.

Re: Reasoning About Program Behavior Algebraically [pdf]

#13

Post by yawaramin »

cmrx64 wrote: post #12
yawaramin wrote: post #11

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 behavio…

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 suggesti…

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.
Post reply on HN