10 ms·
Formal Methods of Software Design an Online Course by Eric Hehner
- deleted 6y ago[deleted]
- ilikeerp 6y agoNo 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.
- gpm 6y agoI'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.
- deleted 6y ago[deleted]
- tra3 6y agoIt it applicable to the "practical" (or practiced?) software development?
- gpm 6y agoI 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.
- iaresee 6y agoI 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.
- shishir03 6y agoDo you have any suggestions for courses teaching practical formal methods?
- exdsq 6y agoThese 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.
- yudlejoza 6y agoThanks for putting it in context. This is exactly what I'm looking for. (making it practical, I'll take care of that myself).
- s_Hogg 6y agoI 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
- madsbuch 6y agoThere 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.
- w_t_payne 6y agoI've been working on something somewhat related. Would be happy to have a chat if you like.
- amichail 6y agoThis course inspired my research on teaching binary tree algorithms using visual programming: https://ieeexplore.ieee.org/abstract/document/545265 https://ieeexplore.ieee.org/abstract/document/545265 http://opsis.sourceforge.net http://opsis.sourceforge.net
- runawaybottle 6y agoI 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 6y agoThe 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.
- runawaybottle 6y agoI guess you are making my point. If the zeitgeist picks up that formal modeling captures intelligence, then it will make its way into the hiring process just like competitive programming did via Leetcode.
- qwertox 6y agoHere 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=PLfsVAYSMwskseQbJ242TApAzA7fW83KyH https://www.youtube.com/watch?v=89fKiaMxHrA&list=PLfsVAYSMws...
- deleted 6y ago[deleted]
- deleted 6y ago[deleted]
- gravypod 6y agoIs there something like this with math? Linear Algebra specifically?
- maniflames 6y agoIf you want to write software using principles from linear algebra you should definitely google some computer graphics courses
- dominicjj 6y agoI 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 6y agoThat 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 https://en.wikipedia.org/wiki/Hoare_logic [1] https://en.wikipedia.org/wiki/Refinement_calculus https://en.wikipedia.org/wiki/Refinement_calculus [2] https://en.wikipedia.org/wiki/Guarded_Command_Language https://en.wikipedia.org/wiki/Guarded_Command_Language
- dominicjj 6y agoGoodness 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 http://p.web.umkc.edu/pgd5ab/cs_451/HW3/hw3.htm
- sn9 6y agoI found mention of "program primes" and "cleanroom" in the index of this book [0], but they are rather far apart from one another. [0] https://svkarthikwinner.files.wordpress.com/2015/07/practical-software-testing.pdf https://svkarthikwinner.files.wordpress.com/2015/07/practica...
- odipar 6y agoI 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!
- PotatoPancakes 6y agoDunno 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 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!
- dang 6y agoOne previous thread: Formal Methods of Software Design: an online course by Eric Hehner - https://news.ycombinator.com/item?id=6464463 https://news.ycombinator.com/item?id=6464463 - Sept 2013 (8 comments)
- EricHehner 6y agoI 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 6y agoMathematical 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.
- mathgladiator 6y agoThat's true, but trust is the way most everything is built outside of academics. Why do we use X framework? Well, because Mr. Deep Pockets over there is using it! I wish we could have a more mathematical world, but it doesn't scale beyond a handful of architects and really talented engineers. The amount of hassle and push back I get for getting 100% code coverage tells me that it's rare for people to leverage more concrete and deeper ideas to even validate their thinking. The market rewards "just ship it" way more because ultimately customers just learn to manage the shit that ships.
- PotatoPancakes 6y agoPlease correct me if I'm mistaken, but I did check a couple of years ago and found what I thought were some errors. I began to draft an email to you but never finished and eventually discarded it. I'll try to recreate it here: With regards to halting, there are some programs that can be written simply in any common programming language to halt iff a solution to a specified number exists, simply by enumerating all possible values and halting if one satisfies the neccessary conditions. Thus to determine the halting of such a program would solve a problem. Typically these can be done in less than ten lines of Python, for instance. Some examples include: does there exist an odd perfect number; do there exist four positive integers a,b,c,n with n>2 such that a^n+b^n=c^n? The former is an open question; and the latter is Fermat's Last Theorem, which took an immense amount of machinery to prove, six decades after Turing's paper, and which is related to many open problems. (I've also heard that the halting problem could be used to solve the Riemann Hypothesis, but I don't know whether or not that's true.) If you can find a way to figure out whether or not such simple programs halt or not, I'd love to hear about it! What I've gleaned from your papers doesn't actually seem to apply to such programs though, which is a shame since these programs aren't very complicated. Now, with regards to Cantor, I recall reading a paper on your website (which I can't seem to find today, so apologies if I misrepresent it). I agree that set theory is not a good way to evaluate the number of numbers, since it throws out all properties about such numbers (e.g. ordering); this is why we have natural density, real density, and other properties. But there was another part where you indicated (something to the effect of) that the reals were countable since there are countably many Turing Machines; however I believe the correct conclusion to draw is that there are uncomputable numbers. Again, I can't seem to find it today, so I apologize if this is unsubstantiated.