IRC channel logs

2019-11-25.log

back to list of logs

<theruran>excellent! :D
<theruran>works 👍
<oriansj>good
<theruran>and you implemented (display)?
<oriansj>yeah
<oriansj>checkout mes_builtins.c to see all of the builtins
<oriansj>(Toward the bottom)
<oriansj>by passing a single list to the primitive it gives me fine grained control of how primitives are expected to behave
<theruran>I like that. It looks good.
<theruran>So why doesn't mes support tail-call optimization?
<oriansj>theruran: we haven't put in the effort
<oriansj>largely because it isn't critical to the bootstrapping problem
<theruran>OK - I wasn't sure if it was excluded from the design
<oriansj>it might be if it makes things faster or simpler
<theruran>right on
<theruran>you might be pleased to know that clang-check only finds 3 warnings here
<oriansj>I'm surprised that there are any warnings
<safinaskar>hi
<safinaskar>oriansj: hi
<vagrantc>janneke: oooh, mes 0.21! hope i can drop some of the debian patches, then. :)
<oriansj>greetings safinaskar
<janneke>vagrantc: yes...i'll announce once savannah is up again
<vagrantc>janneke: there was also a typo in one of the manpages: evalute -> evaluate ... would be nice to catch before release :)
<oriansj>safinaskar: you have concerns about guix's bootstrap; does any code in mescc-tools-seed not seem easy to understand?
<vagrantc>janneke: oh, i already submitted a patch for the typo :)
<janneke>vagrantc: thanks! too late though, -> 0.22 :-)
<oriansj>git commit --amend
<vagrantc>i even sent it to bug-mes in June!
<janneke>oh!
<vagrantc> maybe you've even applied it
<janneke>it's on my list now
<vagrantc>:)
<vagrantc>is there a debbugs for mes ?
<vagrantc>or just the list?
<janneke>no, there's only the list
<janneke>maybe debbugs would be nice, i like it for guix
<oriansj>theruran: ironically I think it might actually be a bug in clang-check *.c -analyze
<safinaskar>oriansj: "any code in mescc-tools-seed not seem easy to understand" - well, i didn't see this project yet. i just came to #guix to ask for this "autoreconf everything" mode
<oriansj>for example if you put require(NULL != i, "Impossible quasiquote processed?\n"); right above the i->cdr = nil; it complains about, the error doesn't disappear; despite the fact it becomes impossible for that code to occur if i == NULL
<safinaskar>oriansj: "then used stage0; it even involves custom hardware" - where is this stage0?
<theruran>oriansj: good catch. These static analysis tools for C can only do so much
<oriansj>safinaskar: it is a non-issue
<oriansj>safinaskar: https://github.com/oriansj/stage0
<theruran>Reading this page and I am horrified by the severity and impact described https://web.archive.org/web/20190921042741/http://wiki.c2.com/?TheKenThompsonHack
<theruran>even worse than I thought
<oriansj>theruran: have you seen the coding machines story yet?
<theruran>oriansj: no. D:
<oriansj>theruran: https://www.teamten.com/lawrence/writings/coding-machines/
<theruran>this is great
<oriansj>theruran: and let us not forget https://www.forbes.com/sites/quora/2014/12/05/what-is-a-coders-worst-nightmare/
<safinaskar>oriansj: well, i looked at stage0. it seems actually as code for custom hardware, but... as well as i understand this hardware doesn't exist in bare metal, right? and we have to emulate it today, right?
<oriansj>safinaskar: well the TTL design hasn't been done because it is a lower priority
<oriansj>There is nothing stopping anyone from implementing it
<safinaskar>oriansj: https://github.com/oriansj/mescc-tools-seed : "any eternal programs" - you actually mean eternal programs or this is a typo?
<oriansj>safinaskar: typo
<oriansj>external is the word
<oriansj>because mescc-tools-seed doesn't even require a shell to be built
<oriansj>the kaem-optional-seed can even be used as an init and bootstrap system and a shell
<oriansj>then fork into that shell to allow you to do as you wish
<safinaskar>oriansj: well, i like your project. and i want to do the same at some point of my life :)
<oriansj>safinaskar: nothing stopping you from helping now
<safinaskar>oriansj: well, right now i am busy with other things. but this project is very interesting. and this is quiet possible i will return to it some day, try to reproduce, probably will report some bugs, patches etc
<oriansj>safinaskar: that is life, just make sure to make time for the things you care about first
<safinaskar>oriansj: :)
<safinaskar>oriansj: and ideally i want to really bootstrap straight from hardware. and this hardware should be build without existing computers
<oriansj>safinaskar: it will be built in TTL (individual NAND, NOR, AND, XOR circuits by hand)
<safinaskar>cool
<oriansj>but an FPGA version will made first to allow for design issues to be detected and corrected
<oriansj>There is even an open call for someone to do an i486 on iCE40 FPGAs
<oriansj>theruran: g_stack = calloc(stack, sizeof(struct cell)); warning however makes less sense given that it is struct cell** g_stack
<oriansj>but atleast I can clear it out by doing sizeof(struct cell*)
<safinaskar>oriansj: https://www.secondwavemedia.com/capitalgains/innovationnews/edustem0831.aspx - is this from you? or just similar name?
<oriansj>safinaskar: an old project
<theruran>oriansj: thanks for looking into it
<safinaskar>oriansj: idea seems strange. also i have hfa
<theruran>why not target a SUBLEQ computer for the stage0 seed?
<safinaskar>oriansj: well, real doctor said me this
<oriansj>theruran: do you want to program a C compiler in that assembly language?
<oriansj>safinaskar: good, use it to your advantage
<theruran>oriansj: oh, by hand? probably not :)
<oriansj>theruran: bootstrapping work is ALL by hand
<theruran>so I guess by your measure of minimalism being cognitive load, SUBLEQ would be too much
<safinaskar>oriansj: what do you like more: lisp or typed functional languages (haskell, ocaml, etc)?
<oriansj>theruran: and I know I can do it on knight: https://github.com/oriansj/stage0/blob/master/stage2/cc_x86.s
<theruran>so Knight is hitting a sweet-spot for comprehensibility?
<oriansj>safinaskar: depends entirely on the problem being solved;
<oriansj>theruran: looking at that assembly, do you feel like it would be hard to make something complex?
<theruran>I guess not. The instruction set seems pretty obvious
<oriansj>There is no perfect tool for building a house, there are times you need a hammer or a saw or a drill
<oriansj>theruran: it is designed to be easy to implement too
<safinaskar>oriansj: i think typed programming languages should be used always except for throw-away tasks
<oriansj>safinaskar: you can't use typed programming languages in the bottom layers of any bootstrap
<safinaskar>oriansj: yes :) but then we should go as quickly as possible to typed ones
<oriansj>safinaskar: and by typed do you mean supporting types like C or real types like Haskell?
<theruran>well I was thinking to bootstrap into KLambda then Shen and use that to write a compiler for DDC. but that just seemed like another one of my crazy ideas :)
<safinaskar>oriansj: strong typing (like haskell) is of course better
<oriansj>theruran: crazy ideas are the ones that flower here; especially if you are willing to do the leg work
<oriansj>safinaskar: so the current haskell bootstrap problem must be a serious concern for you
<safinaskar>oriansj: yes
<theruran>oriansj: I mean, maybe... I think I need to understand more of how this problem of potentially pervasive backdoored tools could affect the claims of my research. If I can't use any off-the-shelf compiler for fear of hidden channels embedded in the output...
<oriansj>safinaskar: good; would you like to help us with that?
<safinaskar>oriansj: well, not now :)
<safinaskar>oriansj: also, i think it is entirely possible to create "typed lisp", i. e. strong static typed language, which is otherwise very similar to lisp, has all its features. i. e. it is simple, homoiconic, has small meta-circular-interpreter (that maxwell equations!), has lisp-style macros, has lisp-like repl
<oriansj>theruran: just use gcc; we will solve that problem for you
<oriansj>safinaskar: yes that is called Haskell's core language
<oriansj>theruran: or figure out how to bootstrap M2-Planet on your arbitrary hardware
<oriansj>because if M2-Planet can be ported to it, you can leverage it's cross-platform verfication capability to prove properties of alternate platforms
<safinaskar>oriansj: haskell has something similar to lisp macros. this feature is called template haskell
<theruran>oriansj: I can't use GCC. Well there is the matter of Independence in Appearance in using tools developed by defense contractors who are funded by superpower governments, such as OCaml by Inria or F# by Microsoft. I think it's highly unlikely the FStar compiler is backdoored but I have no way of proving it outside of this bootstrappable/DDC process. And of course, it could later be backdoored.
<safinaskar>oriansj: but it is not as powerful as lisp macros
<theruran>oriansj: lemme think about that
<safinaskar>oriansj: template haskell cannot be arbitary nested. i. e. there is no analogue of (quote (quote x))
<oriansj>safinaskar: do you really need that do make programs that solve your problems?
<safinaskar>oriansj: also, as well, as i know, this is not possible to construct haskell expression using template haskell and then evaluate it at runtime using "eval".
<safinaskar>oriansj: so i want to create language which is typed, but even more close to lisp than haskell. which has macros with comparable power
<safinaskar>oriansj: so that such language can be ultimate argument against lisp fans. so that i can show it to them and say "this language can do everything your lisp can, but it is typed. so stop using your lisp and use this language instead"
<safinaskar>oriansj: currently i will not do this. i busy with other things. so, you can do this :)
<oriansj>safinaskar: I have no desire to do that; largely because it would not solve a real problem
<oriansj>There are lisp programmers who use haskell and haskell programmers who use lisp.
<oriansj>perfection is a road not a destination
<theruran>One of my goals is to create an FStar-in-LISP which sounds similar to what you describe safinaskar
<oriansj>and every great feature has a cost paid in possibilities
<theruran>You know, because FStar is licensed Apache v2 and requires signing away your copyright to Microsoft through a Contributor License Agreement. That alone is a problem. But it bootstraps from OCaml or F# which is kinda *yikes* from a bootstrappable point of view.
<safinaskar>oriansj: i think it is absolutely possible to create this "typed lisp" such way that its metacircular interpreter will be very small, similar to lisp's one. but it will be typed, so it will be harder to make a mistake in it
<theruran>oriansj: if M2-Planet could be used to write a Shen compiler in a C subset, that could be useful. Currently it requires a huge trusted binary which then self-hosts the Shen compiler to KLambda primitives
<theruran>I still need understand my problem more to layout a detailed plan :/
<oriansj>theruran: well discussing and sharing of thoughts and ideas here make it easier to discover possible solutions
<safinaskar>oriansj: theruran: i once wrote a nearly working checker for https://en.wikipedia.org/wiki/Pure_type_system in haskell
<oriansj>safinaskar: link?
<safinaskar>oriansj: well, unfortunately i was not able to produce bug-free version of pts checker. here is my various attempts: http://safinaskar.com/f/pa.tar . "pts" subdir contains pts checker, which somehow works
<safinaskar>oriansj: other subdirs contain similar checkers for similar languages. programs has tests, so you can try to understand my languages by reading this tests
<oriansj>safinaskar: it is good to see you striving to achieve something interesting
<theruran>oriansj: I guess my plan so far is to write a provably-correct KLambda virtual machine in FStar, and then /somehow/ target that ISA with the FStar compiler to build some verified tools/libraries. That's just temporary though, since I think the long-term path is to use Shen to write a new LISP that reimplements the features of FStar. That would mean bootstrapping Shen from source and applying DDC.
<safinaskar>oriansj: there is pts checker in haskell written by someone else, which is actually working, documented and feature-rich. yarrow: http://web.archive.org/web/20180924133846/http://www.cs.kun.nl/~janz/yarrow/
<theruran>it may sound crazy now...
<safinaskar>my github is github.com/safinaskar
<oriansj>theruran: stage0 still sounds crazy to some people
<oriansj>safinaskar: yes
<theruran>safinaskar: can you ELI5 the benefits of a Pure type system? To me, the Wikipedia article is just describing what it is.
<safinaskar>theruran: this is *very* simple logic foundation. and you can build nearly every other logic on top of it. other logics can be very easily described in terms of it
<safinaskar>theruran: for example, first-order logic, second order logic, higher order logic, simply typed lambda calculi, lambda calculi with dependent types etc
<theruran>safinaskar: such as Shen's sequent calculus which is itself implemented in LISP-embedded Prolog?
<theruran>safinaskar: I have been looking at this the past few days. In Racket I see there is relational logic done in Ocelot. And I was wondering if it makes sense to implement FOL using that. And then wondering how to implement weakest-precondition calculus
<safinaskar>theruran: well, if you want to understand pts, i very recommend this book: https://repository.ubn.ru.nl/handle/2066/17231 . it describes various logics and culminates in pts as generalization of all them
<safinaskar>theruran: i try to describe core idea. in haskell you have terms and types. types themselves have "types" named kinds. theoretically you can kinds have types, too
<safinaskar>theruran: pts is generalization of such idea. you can have arbitrary deep hierarchy with finite or infinite number of levels
<safinaskar>theruran: note that haskell typeclasses can be thought as functions, which take something of kind "Type" and return something of kind "Constraint". this can be described in world of pts, too
<safinaskar>theruran: so, whole foundation of haskell can be just described as list of so-called "sorts" and relations between them
<theruran>safinaskar: that does seem useful because it simplifies the representation, right? thanks for the link, btw
<safinaskar>theruran: yes. it gives very simple and elegant foundation
<safinaskar>theruran: thanks to hurry-coward isomorphism pts can be used both to describe type systems of typed programming languages and to describe logics, which can actually prove mathematical statements
<safinaskar>theruran: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
<safinaskar>s/hurry/curry/
<safinaskar>s/coward/howard/ :)
<theruran>ahh thank you
<safinaskar>theruran: i really recommend you to read whole that book, it is very cool
<theruran>yeah, I need to study up on the formal logic and computation stuffs :)
<safinaskar>theruran: write me safinaskar@mail.ru if you have any questions. i have read that book (nearly) and understand nearly everything. and implemented nearly working pts checker. and know how to describe haskell type system as pts
<theruran>safinaskar: right on :D
<safinaskar>theruran: also, if you want some very simple checker for some logic, which can be implemented as a simple c program, then here is probably what you need: https://www.cs.ru.nl/~freek/aut/index.html
<safinaskar>theruran: also, author of this program, Freek has very informative site, i recommend to read it. notably his comparison of provers: https://www.cs.ru.nl/~freek/comparison/diffs.pdf and other similar works
<theruran>bootstrapping to a proof-assistant, hmm 🤔
<safinaskar>also, pts is simple in sense "small", not in sense "simple to understand"
<safinaskar>theruran: so, you need to understand at first "1st order logic", 2nd order logic, hol, simply typed logic, and other logics and only after them pts as generalization of all them :)
<safinaskar>theruran: so, definitely pts is not thing you should begin with :)
<safinaskar>theruran: but that book is still very good and i recommend it. it goes from simple things (simple to understand) to hard ones
***jonsger1 is now known as jonsger
<safinaskar>bye
<oriansj>it is good to see such passionate people here
<theruran>:)
<theruran>oriansj: mes-m2 builds with CompCert 3.5 and all tests pass. Even the mes-m2 binary is half the size than with my GCC
<oriansj>theruran: the last I checked mes-m2 is looking at 161KB or under (statically compiled)
<oriansj>via M2-Planet
<theruran>104K by hardened GCC 9.2
<theruran>55K by CompCert 3.5
<oriansj>theruran: well it is going to grow as we make it powerful enough to host MesCC and Guix
<oriansj>also slow_lisp with -Os gets down to 44KB
<oriansj>in GCC 9.1.0
<oriansj>so running in L1!
<theruran>oriansj: oops! it was apples-to-apples because I was building without debugging symbols. so 103K from ccomp -g
<theruran>wasn't*
<fosslinux>my L1 is 32K :(
***ChanServ sets mode: +o rekado_
<oriansj>theruran: no worries
<oriansj>fosslinux: Intel chip?
***ng0_ is now known as ng0
***pgreco_ is now known as pgreco
<xentrac>interestingly there's a CP/M small-C compiler also called "MESCC": http://www.floppysoftware.es/c_compilers.html
<janneke>xentrac: wait, what! :-)
<xentrac>I was pretty surprised!
<xentrac>my L1 is 7±2
<fosslinux>oriansj: yes