4 ms·

Thanks for posting this--I'm getting back into studying the formal semantics of programming languages. Questions for those working in this area: According to P

Thanks for posting this--I'm getting back into studying the formal semantics of programming languages. Questions for those working in this area: According to Pierce's Types and Programming Languages, axiomatic semantics of the type that Hoare pioneered are not found as useful today as operational semantics. Is that (still) true? Are the major approaches (operational, denotational, axiomatic) pretty much solidified now, or are there significant new efforts at finding better overall formalizing frameworks?

auggierose 6y ago
There is only one formalising framework, it is called math. The rest is just noise. When trying to make a better framework for formalising computer programs, just make a better framework for formalising math first.
- taeric 6y ago
  Math has many formalisms. Some more useful than others, in certain contexts. All restricted by the norms of communication that they are written in. So, yes, there are some math formalities for processes. No, they probably don't help in finding new processes as much as you'd think. Despite being quite good at understanding existing processes through formal exploration.
- Joker_vD 6y ago
  You can't make a better framework for formalising math, because, as you've yourself said, "there is only one formalising framework", and it's math itself. Cue the problems with self-application and Goedel's tricks :)
  - auggierose 6y ago
    Yeah, in a way you are right. Ok, let me put it this way: Math is not formal. But, formality has its advantages, so what I would like to see is a framework that, while being formal, still allows formulating ideas just as a mathematician would. Kind of like envisioned here: https://www.practal.com https://www.practal.com
Joker_vD 6y ago
Right, the axiomatic semantics aka "the Floyd-Hoare rules". The interesting thing about them is that I've read many presentations of them and not a single one of those had any mention of subroutines (procedures or functions, doesn't matter) at all. All you have is global variables, assignments, sequencing, conditions, and loops. That's it. And while one would think that adding support for subroutines would be tremendously useful, allowing for e.g. specifying correctness of data structures' implementations, apparently it has not been done. The closest thing to it I've seen is TLA+ but holy fatcats is it unwieldy.
- rssoconnor 6y ago
  VerifiableC[1] provides Hoare rules for (a large subset[2] of) C that include function calls, pointers and heap allocation, and some amount of concurrency. It does use an extension to Hoare logic, called separation logic, to achieve some of these features. In particular, separation logic's frame rule is instrumental for the modularization needed for semantics of function calls. [1]https://vst.cs.princeton.edu/veric/ https://vst.cs.princeton.edu/veric/ [2]excludes setjmp/longjmp, unstructured switch statements, goto and maybe a few other moderately exotic constructions.
  - Joker_vD 6y ago
    No goto? Funny, but there is actually a Hoare rule for goto (by Hoare himself), and a rather straightforward one: { pre(L) } S; { P } ------------------------ { pre(L) } L: S; { P } { pre(L) } goto L; { false } You just have to use the same precondition pre(L) for every mention of the label L.
- deleted 6y ago
  [deleted]
rramadass 6y ago
https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/

auggierose 6y ago

There is only one formalising framework, it is called math. The rest is just noise. When trying to make a better framework for formalising computer programs, just make a better framework for formalising math first.

taeric 6y ago
Math has many formalisms. Some more useful than others, in certain contexts. All restricted by the norms of communication that they are written in. So, yes, there are some math formalities for processes. No, they probably don't help in finding new processes as much as you'd think. Despite being quite good at understanding existing processes through formal exploration.
Joker_vD 6y ago
You can't make a better framework for formalising math, because, as you've yourself said, "there is only one formalising framework", and it's math itself. Cue the problems with self-application and Goedel's tricks :)
- auggierose 6y ago
  Yeah, in a way you are right. Ok, let me put it this way: Math is not formal. But, formality has its advantages, so what I would like to see is a framework that, while being formal, still allows formulating ideas just as a mathematician would. Kind of like envisioned here: https://www.practal.com https://www.practal.com

Joker_vD 6y ago

Right, the axiomatic semantics aka "the Floyd-Hoare rules". The interesting thing about them is that I've read many presentations of them and not a single one of those had any mention of subroutines (procedures or functions, doesn't matter) at all. All you have is global variables, assignments, sequencing, conditions, and loops. That's it. And while one would think that adding support for subroutines would be tremendously useful, allowing for e.g. specifying correctness of data structures' implementations, apparently it has not been done. The closest thing to it I've seen is TLA+ but holy fatcats is it unwieldy.

rssoconnor 6y ago
VerifiableC[1] provides Hoare rules for (a large subset[2] of) C that include function calls, pointers and heap allocation, and some amount of concurrency. It does use an extension to Hoare logic, called separation logic, to achieve some of these features. In particular, separation logic's frame rule is instrumental for the modularization needed for semantics of function calls. [1]https://vst.cs.princeton.edu/veric/ https://vst.cs.princeton.edu/veric/ [2]excludes setjmp/longjmp, unstructured switch statements, goto and maybe a few other moderately exotic constructions.
- Joker_vD 6y ago
  No goto? Funny, but there is actually a Hoare rule for goto (by Hoare himself), and a rather straightforward one: { pre(L) } S; { P } ------------------------ { pre(L) } L: S; { P } { pre(L) } goto L; { false } You just have to use the same precondition pre(L) for every mention of the label L.
deleted 6y ago
[deleted]

rramadass 6y ago

https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/