3 ms·
Dafny is a cool language. Conal Eliot, in his 2023 Zurihac talk, says that in order to get efficiency (faster computers that can do more with less) at scale (n
by agentultra 3y ago
Dafny is a cool language.
Conal Eliot, in his 2023 Zurihac talk, says that in order to get efficiency (faster computers that can do more with less) at scale (not merely resilience which we get by adding redundancy and operational tooling) we need languages and tools that allow us to precisely specify the correct program.
Dafny is a good step in that direction. I’m also keen to see where the depedently typed programming languages like Lean 4 and Idris 2 will take us. Proof-carrying code could be very useful.
- practal 3y agoThanks for pointing out the Conal Elliott talk. Just watched it, very nice talk. I found myself nodding to pretty much everything he said, except of his fondness for dependent types. Each time he says "dependent types", I just replace it in my mind with "logic". I think he will transition eventually: Types (Haskell) -> Dependent Types (Agda) -> Logic (Practal), hehehe.
- agentultra 3y agoWell you can encode any logic you want in dependent types, so yeah probably!
- practal 3y agoFair enough. Although to encode a proposition as a type, only to then view it as a proposition again, would be two wrappers too many for my taste. I prefer to keep the notions of truth and types apart. In practice, this makes the logic both simpler and more expressive.
- sn9 3y agoTalk link: https://youtu.be/k6rY5Mvx84E https://youtu.be/k6rY5Mvx84E