From owner-cvs-src@FreeBSD.ORG Sun Jul 27 03:02:42 2003 Return-Path: Delivered-To: cvs-src@freebsd.org Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125]) by hub.freebsd.org (Postfix) with ESMTP id A120F37B401; Sun, 27 Jul 2003 03:02:41 -0700 (PDT) Received: from phk.freebsd.dk (phk.freebsd.dk [212.242.86.175]) by mx1.FreeBSD.org (Postfix) with ESMTP id 00F0843F3F; Sun, 27 Jul 2003 03:02:40 -0700 (PDT) (envelope-from phk@phk.freebsd.dk) Received: from critter.freebsd.dk (critter.freebsd.dk [212.242.86.163]) by phk.freebsd.dk (8.12.8/8.12.8) with ESMTP id h6RA2bV3022429; Sun, 27 Jul 2003 10:02:37 GMT (envelope-from phk@phk.freebsd.dk) Received: from critter.freebsd.dk (localhost [127.0.0.1]) by critter.freebsd.dk (8.12.9/8.12.9) with ESMTP id h6RA2a5H062162; Sun, 27 Jul 2003 12:02:37 +0200 (CEST) (envelope-from phk@phk.freebsd.dk) To: Alexander Leidinger From: "Poul-Henning Kamp" In-Reply-To: Your message of "Sun, 27 Jul 2003 11:54:57 +0200." <20030727115457.553f1df7.Alexander@Leidinger.net> Date: Sun, 27 Jul 2003 12:02:36 +0200 Message-ID: <62161.1059300156@critter.freebsd.dk> cc: cvs-src@freebsd.org cc: src-committers@freebsd.org cc: dds@freebsd.org cc: cvs-all@freebsd.org Subject: Re: cvs commit: src/sys/kern init_main.c kern_malloc.c md5c.c subr_autoconf.c subr_mbuf.c subr_prf.c tty_subr.c vfs_cluster.c vfs_subr.c X-BeenThere: cvs-src@freebsd.org X-Mailman-Version: 2.1.1 Precedence: list List-Id: CVS commit messages for the src tree List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 27 Jul 2003 10:02:43 -0000 In message <20030727115457.553f1df7.Alexander@Leidinger.net>, Alexander Leiding er writes: >> We still have no tools which help us translate high level abstractions >> into low level code or for that matter to validate the high level >> abstractions in the first place. > >Are you talking about e.g. model checking? After Aug 2 I plan to look at >porting 2 major open source model checkers. I don't think you could have gotten an accountant to explain what a spread-sheet would do back in the days before VisiCalc, but once the idea was out, everybody could see that it was brilliant. If I knew what the tools were, I would have been busy writing them years ago, but unfortunately, I don't seem to be the one destined to invent the programmers spread-sheet. >> Given all that, I firmly belive we should embrace every little bit >> of help we can get from tools and programs we have, even if that >> means minor inconveniences and a certain cramping of style here and >> there. > >Perhaps you can convince dds (CCed) to extend devel/cscout in various >helpful directions. Based upon his introduction to us at the time he got >his commit bit and his homepage he may be interested in this kind of >work. I was very happy to see dds@ appear in the asylum :-) -- Poul-Henning Kamp | UNIX since Zilog Zeus 3.20 phk@FreeBSD.ORG | TCP/IP since RFC 956 FreeBSD committer | BSD since 4.3-tahoe Never attribute to malice what can adequately be explained by incompetence.