[cmrx64]

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]

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.