3 ms·
Computing as biology is the (temporary) perspective Alan Kay states in his famous quote: "We don't have a science of software engineering. Until we do, we shoul
by nextos 8y ago
Computing as biology is the (temporary) perspective Alan Kay states in his famous quote: "We don't have a science of software engineering. Until we do, we should take advantage of late binding" [1]
Once we are able to figure out things like model checking, program analysis, abstract interpretation and type systems, we will be able to do computing in a similar way to that of Mathematics. Or at least a bit closer, I think.
[1] http://lambda-the-ultimate.org/node/531 http://lambda-the-ultimate.org/node/531
- gnulinux 8y agoThis is a really bad argument imho. I'm an agda programmer, but only for hobby projects. You can do pretty much everything you listed: "model checking, program analysis, abstract interpretation and type systems" in agda, right now, this very day and some of these stuff is built-in (like dependent type system) or in the standard library. There even is a small industry built around proof automation. But it doesn't follow agda will solve software engineering. When it comes to engineering, it's also about constructing, not just about correctness. Everything you listed solves the latter while ignoring the former. I think the fundamental problem with software engineering is that it is a little too much like mathematics, to the point, the only way to be correct is to be as precise as agda, but, people who practice software engineering, again, just like mathematicians don't care to use this precise language. Just like a mathematician will never write his paper in agda instead of human language, unification will never by itself solve software engineering. Programs are written for humans, not for automated proof checkers, just like papers on mathematics are written for humans.