Conversation

Notices

1. alanz (alanz@mastodon.land)'s status on Thursday, 27-Jul-2017 06:29:04 UTC alanz

   • Christine Lemmer-Webber

   @cwebber have you seen what the deepspec people are up to? Want a proof chain from the app specification to the processor. https://deepspec.org/

   • Hallå Kitteh repeated this.
   • alanz (alanz@mastodon.land)'s status on Thursday, 27-Jul-2017 13:37:18 UTC alanz

     • Christine Lemmer-Webber

     @cwebber It comes up in the latest Functional Geekery podcast too. https://www.functionalgeekery.com/episode-101-adam-chlipala/

     Hallå Kitteh repeated this.
   • Hallå Kitteh (clacke@social.heldscal.la)'s status on Saturday, 29-Jul-2017 02:40:07 UTC Hallå Kitteh

     • Christine Lemmer-Webber
     @cwebber
     
     > Mes is inspired by The Maxwell Equations of Software: LISP-1.5[10]
     
     So that wasn't Byrd's own phrasing. It's almost as old as Computer Science!
   • Hallå Kitteh (clacke@social.heldscal.la)'s status on Monday, 31-Jul-2017 03:03:03 UTC Hallå Kitteh

     • Scheme Programming Language
     • Tomas SA2TMS
     • Christine Lemmer-Webber
     @tomas @cwebber From what I understand the minimal !scheme interpreter in mes is written in assembly, but I haven't dug deeply.
   • Hallå Kitteh (clacke@social.heldscal.la)'s status on Monday, 31-Jul-2017 03:14:29 UTC Hallå Kitteh

     • The Forth programming language
     • Tomas SA2TMS
     • Arun Isaac (அருண் ஐசக்)
     • Christine Lemmer-Webber
     • Elias Mårtenson
     @cwebber @tomas @loke @alanz @arunisaac
     
     http://bootstrappable.org/projects.html explains Mes better in English than the repo or the announcement does, and it also clarifies that mes and stage0 are two different things.
     
     Stage0 apparently starts from almost nothing, goes on with !forth then does some variant of !lisp ... more to study at http://git.savannah.nongnu.org/cgit/stage0.git and http://savannah.nongnu.org/news/?group_id=11718
   • Hallå Kitteh (clacke@social.heldscal.la)'s status on Monday, 31-Jul-2017 03:23:43 UTC Hallå Kitteh

     in reply to

     • Hallå Kitteh
     #hprep trusting trust, stage0, mes ...
   • Hallå Kitteh (clacke@social.heldscal.la)'s status on Tuesday, 01-Aug-2017 08:38:45 UTC Hallå Kitteh

     in reply to

     • Christine Lemmer-Webber
     @alanz @cwebber Listened to it yesterday. Crazy stuff! Proving real-world systems in written horrible languages, synthesising generative testing from incomplete proofs, provable web apps from db to browser ... Breathtaking.
   • Hallå Kitteh (clacke@social.heldscal.la)'s status on Tuesday, 01-Aug-2017 08:39:38 UTC Hallå Kitteh

     in reply to

     • Hallå Kitteh
     written in*
   • Hallå Kitteh (clacke@social.heldscal.la)'s status on Tuesday, 01-Aug-2017 08:42:35 UTC Hallå Kitteh

     • Christine Lemmer-Webber
     @cwebber @thomas Mutual self-hosting may solve trusting trust, but it won't solve the aesthetics of a neat tiny bootstrap object at the bottom of a neat GuixSD package tree. :-)