From mboxrd@z Thu Jan 1 00:00:00 1970 From: Jeremiah@pdp10.guru Subject: Re: Trustworthiness of build farms (was Re: CDN performance) Date: Fri, 04 Jan 2019 20:57:33 +0000 Message-ID: <87va34ywci.fsf@ITSx01.pdp10.guru> Mime-Version: 1.0 Content-Type: text/plain Return-path: Received: from eggs.gnu.org ([208.118.235.92]:45171) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gfWXD-0007Xk-KS for guix-devel@gnu.org; Fri, 04 Jan 2019 15:57:40 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gfWXA-0003i5-GX for guix-devel@gnu.org; Fri, 04 Jan 2019 15:57:39 -0500 Received: from itsx01.pdp10.guru ([74.207.247.251]:38602 helo=itsx01) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gfWXA-0003fp-Ad for guix-devel@gnu.org; Fri, 04 Jan 2019 15:57:36 -0500 In-Reply-To: 87y38auntv.fsf@netris.org List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org Sender: "Guix-devel" To: mhw@netris.org Cc: guix-devel@gnu.org > 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