User loginNavigation 
Applications of formal semanticsI've read this site for some time, but now I have a question I believe the people at LtU could answer. The question is what are some of the current applications of formal semantics. I've read or skimmed through some semantics textbooks, like Winskel's, and some less wellknown, but a question they rarely answer in a satisfactory manner, at least to me, is why I should try to model the semantics of a language formally in the first place. Usually, the books say in the very beginning that semantics is useful for verification and program analysis, and then say no more about it. That's the reason I tried to get hold of a copy of Semantics with Applications as soon as I discovered it (an old edition is available online). The applications mentioned in the book are proving the correctness of an implementation, program analysis, and axiomatic program verification. I've also seen recently the papers about expressing semantics in theorem provers, like here. It's cool that it is possible to extract an interpreter and a module for program analysis from the proofs about semantics. But we could just code the interpreter and program analysis; yes, I know, extracting them from a prover makes them more trustworthy. I refrain from saying that they are "correct" because it would depend on the correctness of the theorem prover, the compiler for the language, the extraction process, etc. Also, I don't know how this idea would fare in bigger, more realistic languages. So, although I have seen already some applications of formal semantics, nothing of it quite managed to impress me much. What is it, then, that we gain by modeling the semantics of a language formally? What we can accomplish with a semantics that we couldn't without? What would be possible without a formal semantics, but difficult and/or clumsy? What examples do we have of sucessful and important applications of formal semantics to programming practice? I think this is very much worth knowing, the questions are worth asking, and the books don't provide answers. So maybe LtU can :) By roberto at 20080413 17:28  LtU Forum  previous forum topic  next forum topic  other blogs  3616 reads

Browse archivesActive forum topics 
Recent comments
3 days 8 hours ago
4 days 8 hours ago
4 days 10 hours ago
4 days 10 hours ago
5 days 16 hours ago
5 days 16 hours ago
6 days 11 hours ago
6 days 13 hours ago
6 days 13 hours ago
1 week 4 hours ago