Path: csiph.com!news.mixmin.net!eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail From: Ben Bacarisse Newsgroups: comp.lang.c++ Subject: Re: [OT] Bad CS course, no cookie Date: Fri, 26 Aug 2022 00:33:50 +0100 Organization: A noiseless patient Spider Lines: 50 Message-ID: <87fshjaof5.fsf@bsb.me.uk> References: <2868500762@darkrealms.ca> <87lerte0qb.fsf@nosuchdomain.example.com> <87sflmszgi.fsf@bsb.me.uk> <87wnaxsofv.fsf@bsb.me.uk> <87r115sn88.fsf@bsb.me.uk> <878rndy1wg.fsf@nosuchdomain.example.com> <87wnaxqsfy.fsf@bsb.me.uk> <87a67sy5u2.fsf@bsb.me.uk> <392fc8fe-b516-434c-8962-c11e2154f4c6n@googlegroups.com> <87y1vcwo4q.fsf@bsb.me.uk> <6aeee22b-9030-481e-86cb-4a47c6746f0bn@googlegroups.com> <871qt4wb6l.fsf@bsb.me.uk> <87pmgoukrd.fsf_-_@bsb.me.uk> MIME-Version: 1.0 Content-Type: text/plain Injection-Info: reader01.eternal-september.org; posting-host="82ff49d57af2f8e7ac36802e47334ae2"; logging-data="3958230"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+akBU01z9lrmObNpEj7y78FssdaQZa7zY=" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) Cancel-Lock: sha1:eSeH+7UKllEsYWQdgasQReE2RYs= sha1:Uiqtv/GRBdq+k+z8dH0OhYDgGSk= X-BSB-Auth: 1.f5dcfe3f8b4f3893b8a4.20220826003350BST.87fshjaof5.fsf@bsb.me.uk Xref: csiph.com comp.lang.c++:86082 David Brown writes: > On 25/08/2022 22:32, Ben Bacarisse wrote: >> David Brown writes: >> >>> When I did theoretical computer science at university, we used >>> whatever type was convenient and appropriate for the task at hand (and >>> more often than not it was "alpha" or "A", rather than any specific >>> type). And that was for "there's no need to test the code, because we >>> prove it is correct on the blackboard" programming, which is as >>> academic as it comes. >> >> Care to name and shame? That's an extraordinary thing to say (if it was >> not a joke)? > > "Beware of bugs in the above code; I have only proved it correct, not > tried it." (Donald Knuth) A well-known quote meaning pretty much the opposite of the remark that piqued my interest. > Several of our courses covered provable code, with mathematical > derivation from specifications through to code. The "programming" > language was somewhat idealised and limited and had no implementation > - the idea was that if you wanted to use the code, you'd translate the > derived algorithm into a practical real language. > > So if you want to look at sorting algorithms, for example, you start > with a list of items of some type (the type does not matter), and a > post condition that the list is sorted. You work through step by > step, with each step justified mathematically, until you have > "executable" code at the end. If you have made no mistakes underway, > you have a proven correct implementation of the specifications - not > just one that has passed some test cases. > > (You can look up the book "Programming from Specifications" by Carroll > Morgan, which is freely available.) There are few books on that sort of topic. Hoare's comes to mind. > I think the only programming language that we were actually taught was > a functional programming language very much like Haskell. When we had > practical work that involved actual programming on computers, we were > expected to learn whatever language the course tutor thought > appropriate for the task - C, Modula 2, and Occam, perhaps more. You could just have said "no"! -- Ben.