[HN Gopher] Introduction to the Theory of Programming Languages ...
___________________________________________________________________
Introduction to the Theory of Programming Languages (1991)
Author : ingve
Score : 187 points
Date : 2022-09-30 06:42 UTC (16 hours ago)
(HTM) web link (bertrandmeyer.com)
(TXT) w3m dump (bertrandmeyer.com)
| siraben wrote:
| For those who are self-studying, I recommend Software
| Foundations[0] which uses the Coq proof assistant, since doing
| the exercises is far more engaging when Coq lets you finish the
| proof and you know for sure that you have understood the concepts
| involved.
|
| [0] https://softwarefoundations.cis.upenn.edu/
| bromuk wrote:
| Did anyone else get taught Eiffel (by Bertrand) when they were at
| University? Such a cool little language for teaching object
| oriented paradigms. I think multiple inheritance was it's selling
| point, never seen it in industry though lol.
| lbriner wrote:
| I never quite got it. We used it for a number of things back in
| the late 90s but to have all of the condition checking enabled
| made it run much slower, which was like most other languages at
| the time, you tested in debug and then released it in release
| mode.
|
| Also, in reference to Ariane rocket explosion
| (https://en.wikipedia.org/wiki/Ariane_flight_V88) due to
| interger overflow, it wasn't clear how a precondition would
| have saved anything - an assertion made by Meyer. If it got to
| the relevant method and the precondition failed, you would
| still have to have forseen the possibility of error and coded
| for it, otherwise it might not have run the function but could
| still have catastrophically failed.
| thenanante wrote:
| Yes, at ETH Zurich. I'm not a big fan of Eiffel, but pre- &
| postconditions + invariants are a great way to verify simple
| functions in isolation. Still needs integration and end-to-end
| tests to verify sufficient correctness in a complex distributed
| environment. On top of that, I really don't like strong OOP. It
| can be misused so easily. Multiple inheritance sounds good in
| theory, but just based on some Java inheritance code nightmares
| I've seen in my career so far, think 10s of layers of deep
| nesting done by misusing inheritance; multiple inheritance
| would massively overcomplicate many codebases. I'm very happy
| the industry seems to move into a pragmatic middle ground,
| where both lightweight OOP and lightweight FP have their uses.
| amval wrote:
| I did! It was not even _that_ long ago. I remember fondly
| reading the Eiffel book by Meyer, which was lenghty but full of
| interest tidbits and explanations.
|
| However, using the language itself was a different story. This
| must have been around 2009. There was barely any documentation
| online, not to speak of libraries. One project required us to
| use some poorly documented, barely functioning and outdated GTK
| bindings.
|
| I think I lacked enough of understanding about programming to
| fully appreciate the language (I remember mostly contracts, as
| something unusual but useful).
|
| I think I will read this book, though: if it's anything like
| the Eiffel one, I am sure it's very fun and didactic.
| anonymousDan wrote:
| Yes! At trinity college in dublin. Very interesting language
| with the pre and post specs.
| zasdffaa wrote:
| I didn't like it. It was too much theory based without enough
| recognition of practice. I and a very small company used it ~25
| years ago. It wasn't good enough & we eventually dumped it. I
| can't give you reasons why as it was too long ago but I don't
| have a good memory of it.
|
| I do remember of the Eiffel book that Meyer was a bit too keen
| on emotive arguments over factual.
| bitL wrote:
| The zeal/tunnel vision of early OOP evangelists resembles the
| zeal of today's FP evangelists...
| zasdffaa wrote:
| (Edited the following)
|
| I'm not talking about OOP. Meyer was hard on pre and
| postconditions (which were massively oversold), but these
| were functionally no more than assertions. He had holes in
| his object system. He had holes in other parts of the type
| system. He was not an object zealot IIRC.
| bitL wrote:
| I took some classes from him while he was at ETH.
| zasdffaa wrote:
| Ok, post modified, but still I don't feel you've
| represented him entirely fairly.
| bitL wrote:
| It could have been interpreted badly - I was just
| pointing out he was from the generation that pushed OOP
| everywhere similarly to FP folks these days, and
| downplaying the problems inherent in Eiffel/OOP,
| similarly to FP folks that see no major issues in their
| own space. A single sentence can't explain the massive
| contribution he had on programming and Agile anyway.
| zasdffaa wrote:
| I misinterpreted it because there's a rash of people who
| post throwaway dismissive stuff (always without any
| justification) and yours looked exactly like that. So, my
| apologies. I'd suggest a mention of your personal
| experience would have been valuable here; actually
| getting lessons off the guy is a big deal.
| smitty1e wrote:
| "The difference between theory and practice is greater in
| practice than in theory."--Herb Sutter
| mejutoco wrote:
| "In theory there is no difference between theory and
| practice - in practice there is" (Yogi Berra)
| cafard wrote:
| "I really didn't say all the things I said." (Yogi Berra:
| https://quoteinvestigator.com/2012/12/30/yogi-didnt-
| say/#:~:...
| pjmlp wrote:
| This is great, must have a paper copy somewhere on my university
| boxes, but it nice that is now available to anyone.
| neebz wrote:
| Bertrand was one of my favorite people in the software field. I
| really wanted to do a Phd under his supervision.
| tailrecursion wrote:
| What gave me the most perspective on programming language design
| was reading Leslie Lamport's papers on TLA+. His views on the
| necessary differences between a P.L. and a specification language
| gave me a clearer idea what programming languages really are. If
| I recall, Lamport has several papers on TLA+ for mere mortals
| that are very easy to read.
| cloogshicer wrote:
| This sounds really great - could you recommend/link some
| specific ones? Thanks in advance!
| tkhattra wrote:
| [1] is a particular one regarding specification languages and
| types. its background description about a "rabidly pro-types"
| referee is quite interesting...
|
| [1] http://lamport.azurewebsites.net/pubs/pubs.html#lamport-
| type...
| cloogshicer wrote:
| So a bit of digging brought up this [1], which seems to be a
| list of all relevant papers.
|
| It's annotated with short summaries and historical background
| by Leslie Lamport himself. Seems like a great starting point!
|
| Still, I'd love to hear some specific recommendations for the
| topic you mentioned, it sounds super interesting.
|
| [1] https://lamport.azurewebsites.net/pubs/pubs.html
| isaacfrond wrote:
| Link to the book:
|
| https://bertrandmeyer.com/wp-content/upLoads/introduction_to...
| ingve wrote:
| Note the warning and request from the main book page:
|
| > (Please do not bookmark or share the above download link as
| it may change, but use the present page:
| https:/bertrandmeyer.com/ITPL.)
| throwaway81523 wrote:
| This book is from 1991. I haven't looked at it, I will do so, it
| looks promising, but my favorite intro(?) PLT book is Robert
| Harper's somewhat idiosyncratic Practical Foundations of
| Programming Languages (PFPL). Some older editions were freely
| available in entirety, and the current edition has an abridged
| version online but they make you pay for the full version.
|
| I found that the older edition was enough to get a handle on the
| subject enough to read other sources.
|
| https://www.cs.cmu.edu/~rwh/pfpl/
| raspberry1337 wrote:
| Any place to read or get this that isn't a preview version?
| [deleted]
| lioeters wrote:
| https://libgen.is/search.php?req=Practical+Foundations+of+Pr.
| ..
| Sakos wrote:
| I use this site too, but it's literally piracy. I don't
| think it should be linked directly on HN.
| oxff wrote:
| my job here is done, was about to reco this too
| kleiba wrote:
| Amazingly, judging from the font rendering, it seems that this
| book was written in MS Word?!
| tengwar2 wrote:
| troff, but MS Word was available from 1983.
| arjvik wrote:
| I know nothing about typography, so could you share which
| aspects of the type specifically stood out to you as bad
| typography?
| LeonidasXIV wrote:
| The fact that it uses Times New Roman gives it a very (old)
| "MS Word" vibe.
| [deleted]
| eru wrote:
| In addition, the text is 'justified', but there's not a
| single hyphenation.
|
| That's what Word does. And it looks a bit ugly. It's
| probably worse than just going with left-alignment.
| layer8 wrote:
| Word actually supports automatic hyphenation, but you
| have to turn it on (it's a property of paragraph styles
| IIRC).
| pjmlp wrote:
| > I was able to reconstruct them from the original troff source
| using plain MS Word.
|
| Also if you look into PDF properties it states the same.
| Pinus wrote:
| The text mentions troff and PIC. I wonder whether the author
| still has the source code... Even if re-rendering with modern
| tools ("modern" meaning "actually runs on platforms readily
| available today, e.g. groff and gpic") is more work than he's
| willing to put in (which I quite understand), there ought to be
| _someone_ on the Internet who is enough of a compsci
| /typography nerd to do it...
| sambeau wrote:
| This was on one of my set texts at University in the 1990s. I
| still own it (somewhere) and a few others in this series. There
| was a companion book by David Watt which covered the
| implementation of interpreters and compilers and used a small
| functional language that looked a little bit like Pascal, called
| Triangle. It was written in very plain, easy-to-understand
| language (and the code was simple to understand, too). I have
| Peyton Jones's 'The Implementation of FunctionalProgramming
| Languages' sitting on a shelf beside me, and I often like to look
| back at Bird & Wadler which is a classic, though I think I lent
| it to someone and never got it back.
| candyman wrote:
| We used Eiffel to build a funds transfer system way back when,
| Maybe 1990 or so. I met Bertrand a couple of times because my
| mentor was a huge fan. He built systems in banking using Modula-2
| before Eiffel came along. Last I saw Bertrand he was in Santa
| Barbara. It feels like disciplined programming is not popular
| anymore in favor hacking, continuous releases, agile, scrum, etc.
| asib wrote:
| What makes you say continuous deployment, agile, scrum are in
| contest with disciplined programming? Maybe I'm misinterpreting
| the meaning of that term.
| rramadass wrote:
| >It feels like disciplined programming is not popular anymore
| in favor hacking, continuous releases, agile, scrum, etc.
|
| Rightly said!
|
| I learnt "correct" OOD/OOP from his book _Object-Oriented
| Software Construction_ (https://bertrandmeyer.com/oosc2/). It
| was one of the few books which actually looked at "Programming
| in the Large" specifically through the Object-Oriented lens and
| also instituted "Design By Contract (DbC)" within the Eiffel
| language to support it. DbC is a "user-friendly" version of the
| correct programming techniques espoused by
| Floyd/Hoare/Dijkstra. One can also say that it subsumes other
| techniques like TDD since a post-condition is like a unit test
| in itself. It is a shame people no longer study Meyer's works
| with the seriousness they should (he maybe a pedant but it is
| the right sort of pedantry) but instead run after buzzwords/fad
| of the month.
|
| Here is Bertrand Meyer's take (the right one, imo) on Agile
| from his book _Agile! The Good, the Hype and the Ugly_ -
| https://learning.acm.org/techtalks/agile.
| mindcrime wrote:
| _disciplined programming is not popular anymore in favor
| hacking, continuous releases, agile, scrum, etc._
|
| Wait what? Disciplined programming is not mutually exclusive
| with at least 3 of those 4 things (continuous releases, agile,
| scrum). If people treat those things as opposed to disciplined
| programming, it's because they don't understand the actual
| principles underlying them.
| amelius wrote:
| This title assumes that there is a single theory of programming
| languages, which is a bit strange.
| jonsen wrote:
| Not at all:
|
| https://en.m.wikipedia.org/wiki/Programming_language_theory
| nudpiedo wrote:
| I see it is mostly focused on semantics: operational,
| translational, denotational, axiomatic, complementary.
|
| I wish there were more books focused on that aspect. I will
| definitely take a look at it over the weekend.
| mkehrt wrote:
| For a good look at type theory and its relationship to
| operational semantics in particular, Pierce's Types and
| Programming Languages is the classic. I suspect Harper's
| Practical Foundations for Programming Languages has a similar
| approach though I've not read it.
| rramadass wrote:
| 1) _Formal Syntax and Semantics of Programming Languages: A
| Laboratory Based Approach by Kenneth Slonneger and Barry Kurtz_
| - https://homepage.divms.uiowa.edu/~slonnegr/ (PDFs are
| available on the web).
|
| 2) You may also find Cliff B. Jones' book _Understanding
| Programming Languages_ useful.
|
| Excerpt from the preface;
|
| _Fortunately, there is a less expensive way of sorting out the
| meaning of a programming language than writing a compiler. This
| book is about describing the meaning (semantics) of programming
| languages. A major objective is to teach the skill of writing
| semantic descriptions because this provides a way to think out
| and make choices about the semantic features of a programming
| language in a cost effective way. In one sense a compiler (or
| an interpreter) offers a complete formal description of the
| semantics of its source language. But it is not something that
| can be used as a basis for reasoning about the source language;
| nor can it serve as a definition of a programming language
| itself since this must allow a range of implementations.
| Writing a formal semantics of a language can yield a far
| shorter description and one about which it is possible to
| reason. To think that it is a sensible engineering process to
| go from a collection of sample programs directly to coding a
| compiler would be naive in the extreme. What a formal semantic
| description offers is a way to think out, record and analyse
| design choices in a language; such a description can also be
| the basis of a systematic development process for subsequent
| compilers. To record a description of the semantics of a
| language requires a notation --a "meta-language". The meta-
| language used in this book is simple and is covered in easy
| steps throughout the early chapters._
___________________________________________________________________
(page generated 2022-09-30 23:02 UTC)