Re: Trustworthiness of build farms (was Re: CDN performance)

[Jeremiah]

> Where are you getting those complexity expressions from?
Approximation of developer effort spent on single pass workflows and
bugfree libraries in the State of Michigan Welfware Eligibility System
extracted from it's ClearCase commit history. (Thank god, I finally got
them to convert to git after 3 years of wailing and gnashing of teeth)

> Can you cite references to back them up?
I can site the numbers I used to generate those approximate complexity equations

> If not, can you explain how you arrived at them?
Simple graphing and curve matching of collected data.

> What is 'c'?
Number of 'Features' a program had.
In short I found it is far easier for a developer to add features to a
program but it is really really hard to make sure the existing
functionality is bug free.

> If you're referring to the bugs found in CompCert, the ones I know about
> were actually bugs in the unverified parts of the toolchain.
I was referring to the bugs in the verified parts in regards to C's
undefined behavior.

> In the past, its frontend was unverified, and several bugs were found there.
> Even today, it produces assembly code, and depends on an unverified
> assembler and linker.
Which depending on if the compiler has been formally proven to only
output valid assembly (no 33bit offset loads) then that is less of a
concern.
(Let us just hope the assembler doesn't arbitrarily choose 8bit
immediates for performance reasons when given a 32bit int)

> Bugs can also exist in the specifications themselves, of course.
The most important class of bugs indeed

> I'm not sure what "and human model first behavior" means, but if you
> mean that the semantics of languages should strive to match what a human
> would naturally expect, avoiding surprising or unintuitive behavior, I
> certainly agree.
That is exactly what I mean. The problem is ultimately do be useful
things one has to support things that violate that in very terriable
ways (like support IEEE floating point, disable garbage collection, etc).

> I consider Standard ML, and some subsets of Scheme and
> Lisp, to be such languages
They certainly do have wonderful properties but I wouldn't say they
qualify as matching the human model first behavior requirement (easy to
verify by doing the 50 non-programmers first hand test)

Ask a room full of non-programmers to use scheme to write a standard web
CRUD app using an SQLite3 database backend or do XML parsing or generate
a pdf/excel file. It doesn't look pretty and most just give up on the
offer of free money after a bit.


> If I understand correctly, what you don't expect to happen has already
> been done.  CakeML is free software, and formally proven correct all the
> way down to the machine code.  Moreover, it implements a language with
> an exceptionally clear semantics and no undefined behavior.
I don't deny that the CakeML team did an excellent job on their formally
verified backend and their type inferencer. Most humans are not
programmers and of the programmers, most of them programming by proof
isn't in the realm of intuitive. 

> Anyway, you've made it fairly clear that you're not interested in this
> line of work, and that's fine.
It isn't so much as not interested but rather it is lower on my priorities

> I appreciate the work you're doing > nonetheless.
As I appreciate the work you do as well.

-Jeremiah