3 ms·

> As computer-assisted proofs become more and more popular, expect plenty of cross-polination between software engineers and Mathematicians. Similar things wer

by davesmith1983 7y ago

> As computer-assisted proofs become more and more popular, expect plenty of cross-polination between software engineers and Mathematicians. Similar things were said in the 1950s and 1960s. I don't remember specifics but our lecturers told us that computer scientists back then thought that they could actually just mathematically express a program and there would be no need for a programmer. The Vienna Development Method has been around for god knows how many years and have never caught on. Saying that programming is like maths, is the same as saying cooking is like chemistry. Sure there is lots of chemistry going on in the food, but I doubt many chefs know or care about the chemical properties of organic compounds. Additionally we actually did a course on VDM back in 2006/2007 and the lecturer said that he had only encountered one team that proved their program to be correct and it took them about a decade. You could argue the code itself is the mathematical expression. But honestly as someone that has a very strong Maths background and moved to Software Engineering most software unless you are doing something very specific like a sorting algorithm a lot of code isn't really that algorithmic, you are in the vast majority of cases just expressing a set of business rules and that is in my experience is best described by Use Cases / User Stories. For most businesses this is simply a waste of time. Getting developers to write tests is hard enough and businesses don't see the benefit until things start going horrifically wrong.

YeGoblynQueenne 7y ago
So, I remember once as a junior dev, I was asked to write a SQL script to get some data from some tables, etc. I wrote the script and it was taking for ever to run. I scratched my head, had a close look and it was obvious that my script was running in quadratic time (plus, you know- expensive joins and stuff). I rewrote it to run in linear time and, hey, presto- the job was done in a flash. That is how programmers use maths to do their everyday work. Note that I don't mean you need to know that what you're doing is asymptotic analysis and so on to optimise your code when it gets bogged down in unnecessarily expensive compuations, but even if you don't call what you do what it is formally known as, you are still doing that thing. And that thing is called "using maths".
ukj 7y ago
It always boils down to use-cases. Ultimately, what formal verification gives you is a guarantee of structural correctness, but not behavioural correctness. Whether a program behaves as intended or required is still a task for humans. Garbage in - garbage out. Whether structural correctness is a requirement is a function of the software's criticality and purpose. You probably don't need it for your blog... There is one critical FYI. If you require formal verification of your code you have to give up Turing-completeness. https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming

YeGoblynQueenne 7y ago

So, I remember once as a junior dev, I was asked to write a SQL script to get some data from some tables, etc. I wrote the script and it was taking for ever to run. I scratched my head, had a close look and it was obvious that my script was running in quadratic time (plus, you know- expensive joins and stuff). I rewrote it to run in linear time and, hey, presto- the job was done in a flash. That is how programmers use maths to do their everyday work. Note that I don't mean you need to know that what you're doing is asymptotic analysis and so on to optimise your code when it gets bogged down in unnecessarily expensive compuations, but even if you don't call what you do what it is formally known as, you are still doing that thing. And that thing is called "using maths".

ukj 7y ago

It always boils down to use-cases. Ultimately, what formal verification gives you is a guarantee of structural correctness, but not behavioural correctness. Whether a program behaves as intended or required is still a task for humans. Garbage in - garbage out. Whether structural correctness is a requirement is a function of the software's criticality and purpose. You probably don't need it for your blog... There is one critical FYI. If you require formal verification of your code you have to give up Turing-completeness. https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming