From owner-freebsd-hackers@freebsd.org Mon Dec 31 18:40:28 2018 Return-Path: Delivered-To: freebsd-hackers@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 348A5143C992 for ; Mon, 31 Dec 2018 18:40:28 +0000 (UTC) (envelope-from rigoletto@FreeBSD.org) Received: from smtp.freebsd.org (smtp.freebsd.org [96.47.72.83]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) server-signature RSA-PSS (4096 bits) client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "smtp.freebsd.org", Issuer "Let's Encrypt Authority X3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id D07D177E92 for ; Mon, 31 Dec 2018 18:40:27 +0000 (UTC) (envelope-from rigoletto@FreeBSD.org) Received: from privacychain.ch (unknown [179.35.96.225]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) (Authenticated sender: rigoletto) by smtp.freebsd.org (Postfix) with ESMTPSA id 36F3B1A884 for ; Mon, 31 Dec 2018 18:40:27 +0000 (UTC) (envelope-from rigoletto@FreeBSD.org) Date: Mon, 31 Dec 2018 16:40:22 -0200 From: Alexandre =?utf-8?Q?C=2E_Guimar=C3=A3es?= To: freebsd-hackers@freebsd.org Subject: Re: Speculative: Rust for base system components Message-ID: <20181231184022.sw2evxodjwwmmtup@privacychain.ch> References: MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="n3octopd3uwn3giv" Content-Disposition: inline In-Reply-To: User-Agent: NeoMutt/20180716 X-Rspamd-Queue-Id: D07D177E92 X-Spamd-Bar: ------ Authentication-Results: mx1.freebsd.org X-Spamd-Result: default: False [-7.00 / 15.00]; NEURAL_HAM_MEDIUM(-1.00)[-1.000,0]; NEURAL_HAM_SHORT(-1.00)[-0.997,0]; REPLY(-4.00)[]; NEURAL_HAM_LONG(-1.00)[-1.000,0] X-BeenThere: freebsd-hackers@freebsd.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Technical Discussions relating to FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 31 Dec 2018 18:40:28 -0000 --n3octopd3uwn3giv Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Hi. Just to add my 2c. ;-) If the objective is *security* and *reliability*, the said options: C++=20 (assuming HIC++), Rust, and Haskwell are all surpassed in these regards by= =20 Ada/SPARK (yes, there is the compiler problem) and OCaml, both in fact used= =20 by high integrity safe-critical industries. There is a new Ada standard coming (Ada2020), and the Ada standard=20 `updates` are not the hell of C++ ones. The SPARK language is being formally verified by INRIA using the Coq proof= =20 assistant (which is written in OCaml). http://sworthodoxy.blogspot.com/2017/03/comparing-ada-and-high-integrity-c.= html PS. oh, there is also a CompCert frontend being written for SPARK by INRIA= =20 (at least they were prototyping it in 2014). Cheers! --=20 Best Regards, Alexandre C. Guimar=C3=A3es. https://bitbucket.org/rigoletto-freebsd/ --n3octopd3uwn3giv Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQKTBAEBCgB9FiEE9RbDjoZ0ELBWamGCmSH8wDhAF9kFAlwqYpFfFIAAAAAALgAo aXNzdWVyLWZwckBub3RhdGlvbnMub3BlbnBncC5maWZ0aGhvcnNlbWFuLm5ldEY1 MTZDMzhFODY3NDEwQjA1NjZBNjE4Mjk5MjFGQ0MwMzg0MDE3RDkACgkQmSH8wDhA F9n5NhAAy71W/LjiWGiBMujCvYh4LMZC0QKJ43FGgujW8rlFSia5J4JUYykQmhQO Dnv9ggooXJyggPwsu29Q2pD9FvY5qT8skDZmFiYumgcvJ5TKnoUpPl4lTOyhCZN7 Bif4iCUH56Whwebkhhlu4KjyMFqNVrzooDXUCiUl+tm5KEH/9KAV6OVinYieQsqc r51Re/MqzDcn8xjyr2zUvkHy8BTmKvClZq8nM7nPSAi9/EmYPoC/XK2zRbUNQcua BKUBhXHh3uhpUXVUpHFHevcKEFACt83r0VbbWmi76GBns1TMspFr4lCllQ37orsJ Kvk1jOJ9eSfdNFElrnpbBCHAs/DcImiOwlhvGH406L392digAuhFzRYoJvfv3xt8 7dTT7nOj2mTrzadRjKe2nMn0dK7aftRLAWKGwuTEhkEj7L1QQT+4o+jiVOwNz5B0 5X1QXcfGic5t+TqfT3JLEpmCFbaENH+bYSq9hs11dZZo1W+hMRdYkH+CwmACmN0C +WMQ0r/jpjVSN7rxmanVLd7YBQfqHOyQ3OaZlHXqCsS3L3dXXQji6B0rGB0P263g 9oyT1vHuuTFBbVDObj8gZVcDhsasmQhvl/mKtF+8ODaYo7XZHiF8E2kQlrPgjSHW WyjCVhGD963jT/4u3DoyR888N/XaSNh47FsmPDLVRFRWZREVRGk= =D4m2 -----END PGP SIGNATURE----- --n3octopd3uwn3giv--