On Mon, 02 May 2016, Marc Collin <marc.collin7_AT_gmail.com> wrote:
> Something better than using fancy (aka: complex) languages with
> garbage collector, memory safeness, etc. is to formal verify your C
> program[0]. There's even a kernel, seL4 that's been formally verified
> to not contain certain bugs like buffer overflow and that kind of
> stuff.[1]
Related:
https://coq.inria.fr/
> [...] when von Neumann found out about it he was very angry, saying
> that it was a waste of a valuable scientific computing instrument to
> use it to do clerical work.
This simply does not make any economical sense. You either:
1. Have all people do clerical work;
2. Build computer systems, offloading some of the clerical work to
programmers by using $LANGUAGE, making group 1 more productive;
3. Offload the hard problems in 2. to compiler / language developers,
making group 2 more productive (and by proxy, also group 1).
Sooner or later you end up with 3, because the businesses that don't
embrace it, lose their competitive advantage to businesses that do.
This is fine, it's called progress, it makes life better. Whoever
disagrees: you're free to live in a cave.
What's not fine is unbound complexity. But this gets dealt with once in
a while all on its own, again, regulated by the free market and the
costs of sticking to solutions that suck too much. HTTP+JSON, Unix, Go,
are all good examples of a simpler technology displacing a bunch of
unnecessarily complex competitors.
K.
Received on Mon May 02 2016 - 14:48:42 CEST