[HN Gopher] Formal Methods of Software Design an Online Course b...
___________________________________________________________________
Formal Methods of Software Design an Online Course by Eric Hehner
Author : blewboarwastake
Score : 239 points
Date : 2021-03-28 13:30 UTC (9 hours ago)
(HTM) web link (www.cs.utoronto.ca)
(TXT) w3m dump (www.cs.utoronto.ca)
| EricHehner wrote:
| I may be notorious, but not for the work I've done, rather for
| the misinformation about me that is repeated by people who don't
| check. I have written and published papers that say halting for
| programs in one formal system (language) cannot be solved in that
| same system, but can be solved in a different formal system. I
| would be delighted if you find an error in that work, but no-one
| has done so yet. I have never said that Goedel was wrong; I have
| written a paper explaining Goedel's results that other authors
| have used in textbooks and translations. I have never said
| Cantor's proof is wrong, but I have suggested there are other
| measures of set size than the one he proposed.
| EricHehner wrote:
| Mathematical results should never be accepted or rejected by
| whether you "trust this guy". You should read the work, think
| about it, and decide for yourself whether the results are right
| or wrong.
| [deleted]
| s_Hogg wrote:
| I wonder if anyone has some thoughts on the application of
| methods like this in the realm of machine learning modelling? I'm
| very interested in the concept and can see there must be a link
| but haven't yet thought my way into it
| w_t_payne wrote:
| I've been working on something somewhat related. Would be happy
| to have a chat if you like.
| madsbuch wrote:
| There is a bit of research going on in the space between
| programming languages and machine learning. Mostly it is about
| probabilistic programming and Bayesian methods etc.
|
| However, using type theory to assist in writing models is
| something I am currently looking into. It is an interesting
| area that has the potential to propel the development of
| seriously large models.
| gravypod wrote:
| Is there something like this with math? Linear Algebra
| specifically?
| maniflames wrote:
| If you want to write software using principles from linear
| algebra you should definitely google some computer graphics
| courses
| dang wrote:
| One previous thread:
|
| _Formal Methods of Software Design: an online course by Eric
| Hehner_ - https://news.ycombinator.com/item?id=6464463 - Sept
| 2013 (8 comments)
| [deleted]
| dominicjj wrote:
| I laughed at formal methods of program proof until I came across
| a simplified version of cleanroom development methodology (which
| breaks program components into 'program primes' like A then B, If
| A then B, While A do B and for A in B do C) that allowed you to
| formally prove outcomes on paper. I have long since lost the
| document but to this day, I construct most of my work around
| these primes for certain projects.
| Jtsummers wrote:
| That sounds a bit like Hoare logic [0], refinement calculus
| [1], or guarded command language [2]. The term "program prime"
| is not something I've heard or read before and I'm not turning
| up much.
|
| [0] https://en.wikipedia.org/wiki/Hoare_logic
|
| [1] https://en.wikipedia.org/wiki/Refinement_calculus
|
| [2] https://en.wikipedia.org/wiki/Guarded_Command_Language
| dominicjj wrote:
| Goodness knows why my original comment is being downvoted.
| The formal term is 'primary program refinement' and can be
| found all over the place such as here:
|
| http://p.web.umkc.edu/pgd5ab/cs_451/HW3/hw3.htm
| amichail wrote:
| This course inspired my research on teaching binary tree
| algorithms using visual programming:
|
| https://ieeexplore.ieee.org/abstract/document/545265
|
| http://opsis.sourceforge.net
| ilikeerp wrote:
| No comments because everyone here is a JS, break it until you
| make it, sort of developer with no real responsibilities.
|
| Thanks for the downvotes you aspie, racist, and sexist spastics.
| runawaybottle wrote:
| I want to say stuff like this will never show up in your career,
| but then competition level algos started showing up in the
| interview.
|
| Might be a chance to get ahead of the curve here, bookmarked.
| This looks interesting and challenging, but maybe not realistic.
| Prime candidate to grind out 1000s of these exercises.
| Supermancho wrote:
| The vast majority of developers will never encounter this stuff
| in the way it's being presented. Sometimes you'll be hacking
| together some version of a js framework to get some UI feature
| using the patterns permitted by company A in a very narrow
| scope. In a practical sense, that's not using the concepts as
| much as stumbling across them.
| gpm wrote:
| I've done this course. It's interesting and makes you think,
| would recommend if that's what you're looking for.
|
| While not my area of expertise, I don't this course is
| particularly relevant to any practical modern formal methods
| unless you want to reinvent the world.
| yudlejoza wrote:
| Thanks for putting it in context. This is exactly what I'm
| looking for. (making it practical, I'll take care of that
| myself).
| shishir03 wrote:
| Do you have any suggestions for courses teaching practical
| formal methods?
| exdsq wrote:
| These aren't courses, but I recommend looking at TLA+ and
| Alloy. Some of my colleagues use Isabelle, Coq, and Agda too,
| but the first two seem most relevant to learn.
| gpm wrote:
| I've also heard good things about lean.
| exdsq wrote:
| I forgot about Lean, but yeah I've heard good things too!
| Hillel Wayne has a good email list I recommend where he
| sends weekly posts on different tools :)
| [deleted]
| iaresee wrote:
| I took both the intro and advanced version of this course in my
| undergrad. Academically interesting stuff, but the inability to
| translate from proved system to implemented and proved system
| was always frustrating.
|
| It was definitey a clear delineation between _computer science_
| and _engineering science_ during my undergraduate courses.
| tra3 wrote:
| It it applicable to the "practical" (or practiced?) software
| development?
| gpm wrote:
| I wouldn't say so, maybe slightly in that it might help with
| thought patterns a bit, but in the way that studying advanced
| mathematics might help not as in you're likely to directly
| use the skills.
| PotatoPancakes wrote:
| Dunno how much I trust this guy. He's notorious for claiming that
| the Halting Problem is actually solvable, and in other places
| suggests that Godel was wrong, and even that Cantor's proof that
| the reals are uncountable is wrong.
| http://www.cs.toronto.edu/~hehner/halting.html Finding the flaws
| in all those arguments is a good challenge if you have a free
| afternoon!
| gpm wrote:
| He's somewhat of a crank, but the math in this course is
| approachable and correct, and the ideas interesting. It was
| also created... awhile ago.
| qwertox wrote:
| Here is a YouTube playlist, for those who don't want to download
| the individual *.mov-files and are OK with streaming via YouTube.
|
| https://www.youtube.com/watch?v=89fKiaMxHrA&list=PLfsVAYSMws...
| odipar wrote:
| I really like Eric's work, especially "From Boolean Algebra to
| Unified Algebra".
|
| His algebraic approach towards building software is really
| refreshing as it starts with the absolute basics and then slowly
| builds to a whole framework. Recommended!
| [deleted]
___________________________________________________________________
(page generated 2021-03-28 23:01 UTC)