<KipIngram>
remexre: they eventually got around to explaining, and I'm grokking it ok so far.
boru` has joined #forth
boru has quit [Disconnected by services]
boru` is now known as boru
mark4 has joined #forth
boru` has joined #forth
boru has quit [Disconnected by services]
boru` is now known as boru
dave0 has joined #forth
<dave0>
maw
<siraben>
KipIngram: that's interesting yes, I would only recommend people learn computing like that if they really are learning CS as their main pursuit
<siraben>
I'm reminded of helping a finance major who was taking CS as a minor learn about state machines and logic gates for a class and she ended up dropping the minor :(
<siraben>
it's just a lot to handle when CS is not one's main pursuit
<siraben>
KipIngram: re: peano arithmetic, you're right, it's very far removed from actual arithmetic, and even in the FP community no one uses it, but it's the simplest number system that also has a simple inductive principle
<siraben>
what happens in practice is binary numbers are encoded, the equivalence of unary and binary number systems is established and all the proofs can get carried over for free from the unary world
<siraben>
DKordic: fix FTW, I was concerned about its metatheoretical properties but denotational semantics just says it's the least fixed point
<siraben>
it's quite something to see the semantics of a while loop expressed as a least fixed point
<siraben>
> For example, it says that "f compose g" is (Lvwx.v(wx))fg where L is the lambda.
<siraben>
read that as (define (compose f g) (((lambda (v) (lambda (w) (lambda (x) (v (w x))))) f) g))
<siraben>
I guess you can see why that notation is superior to this :P
rixard has quit [Read error: Connection reset by peer]
rixard has joined #forth
sts-q has quit [Ping timeout: 246 seconds]
<DKordic>
KipIngram: My "dfn" of "Forth!" is a Composition.
<DKordic>
siraben: Semantics of Natural Numbers?!
<DKordic>
Let Us start with them. Or something else?
gravicappa has joined #forth
<siraben>
DKordic: What do you mean semantics of natural numbers?
sts-q has joined #forth
gravicappa has quit [Ping timeout: 245 seconds]
<DKordic>
siraben: I can not remember any statement mentioning semantics that made any sense to me. I completely disagree ""peano arithmetic"".
<DKordic>
siraben, KipIngram: Show me some simple add, sub, mul, and div Implemented as Combinators .
<DKordic>
siraben: Your (most recent) ""compose"" is Scheming.
<siraben>
DKordic: yes it's scheme, for kipgram is more familiar with that syntax
<siraben>
DKordic: peano arithmetic is simple, that's really all there is to it, it's not designed for efficiency
<DKordic>
What might be wrong with it?
<siraben>
What criteria are you judging it by?
<siraben>
simple inductive principle: to show something holds for all peano numbers, show it's true for 0, and show it's true for k+1 assuming it's true for k, then it's true for all n
<DKordic>
My question about ""compose"" is not about ""syntax"". (IMHO) Your statement about ""efficiency"" of ""peano arithmetic"" is _not even wrong_.
mtsd has joined #forth
wineroots has joined #forth
andrei-n has joined #forth
<siraben>
KipIngram: oh yeah, the _only_ thing you can do in lambda calculus is substitution
<siraben>
remexre: I'm working through Programming Languages Foundations now and it's nice to be able to formulate Hoare logic and use it to show imperative programs satisfy a desired behavior
<remexre>
oh, nice; my reading group gave up after the Equiv chapter
mark4 has quit [Quit: Leaving]
mark4 has joined #forth
<remexre>
(nothing against that chapter, we'd just been doing coq for months and some people had dropped out from being sick of it)
phadthai_ is now known as phadthai
jedb has quit [Quit: Leaving]
jedb has joined #forth
gravicappa has joined #forth
<siraben>
remexre: I had to grind through Equiv, I'm not totally done with it (the exercises involving the HAVOC construction were much harder because you couldn't just finish the proof by using determinism of evaluation)
<siraben>
I think the verified functional algorithms chapter is a nice progression from vol 1.
<siraben>
much more automation which makes you feel better about scaling up your proofs
<siraben>
vol 1 and 2 have quite manual proofs
<DKordic>
One has to be sick in order not to get sick from Coq.
<siraben>
DKordic: what do you mean?
<DKordic>
Coq is good for nothing!!
<siraben>
you are being hyperbolic?
<siraben>
are you*
<DKordic>
IMHO Coq is an application of Ad Nauseum, like UNIX was for hardware of it's day.
<siraben>
I don't understand, do you work directly with Coq? It's used for a wide variety of applications
<siraben>
Certainly it's been used to formalize many famous non-trivial results in mathematics
<siraben>
(this would perhaps be a better conversation to have in #coq)
<siraben>
DKordic: It would be nice if you elaborate it on its perceived technical shortcomings
<DKordic>
siraben: I might be wrong. Please enlighten me with some introductory examples.
<siraben>
DKordic: I'm not understanding what aspects you are criticizing
<siraben>
I can address those specific points perhaps
<DKordic>
What is straightforward in Coq?
<siraben>
DKordic: well that depends on your experience and prior knowledge
<siraben>
What's straightforward in Forth, or C++? for instance
<siraben>
maybe it would be good to motivate why coq (or any other theorem prover) is needed in certain domains
<siraben>
in mathematics, mistakes in proofs can be catastrophic especially if more work depends on it, directly or indirectly, and having machine-checked proofs guarantees the proof is valid
<siraben>
in programming language theory, similarly, soundness & completeness proofs of type systems can get pretty hairy, and you can also machine-check the proofs to be completely sure
<DKordic>
I would like to "PowerON" my Computer into a Forth REPL. Then do everything from there.
<siraben>
I thought we were talking about the purpose of Coq?
<siraben>
I don't understand what you mean when you say "Coq is good for nothing", I would like to hear you elaborate
dave69 has joined #forth
<cess11>
never heard about proof assistants implemented in forth, is there one with public source?
dave0 has quit [Disconnected by services]
dave69 is now known as dave0
<remexre>
I'd imagine you could implement something like Abella in Forth "without an extraordinary amount of work"
<remexre>
but it's not really "native ground," so to speak; you're usually doing a bunch of term manipulation, which imo works best with a GC,
<remexre>
s/,$//
<siraben>
remexre: I've wanted to formally verify compilation to a stack machine for a while, should be a fun exercise
<siraben>
for expressions it's easy, with control constructs it's a bit harder
<remexre>
yeah, ditto; I've been meaning to try and write up a semantics for my forth, prove my implementation correct against the ARM ASL spec, then start proving things about programs
<siraben>
don't know if I should add a return stack as well heh, that does make things even harder
<remexre>
I think that if I "dip down to" the machine level, it should make control constructs (and hardware interactions!) much easier
<siraben>
oh great, what about a virtual machine?
<siraben>
or yeah you could again relate the VM against ARM
<siraben>
and compose the proofs
<remexre>
yeah
<KipIngram>
Yes, I see that Peano arithmetic supports a simple logical principle. I guess I'm just willing to accept arithmetic as "obviously correct." Maybe that's just a difference between an engineering field and a theoretical field - when going for an engineering knowledge you don't necessarily feel compeled to prove things from the *very* ground floor. You choose a "pragmatic starting point."
<KipIngram>
But I see that that's not appropriate for full mathematical rigor.
<siraben>
remexre: if you undertake the project let me know, i would want to contribute proofs and such as well
<siraben>
KipIngram: correct, for embedded I guess the hardware is taken as trusted according to the spec
<siraben>
and they do indeed use formal methods to check correctness of chips! (at least intel and AMD do)
<siraben>
remexre: I think for verifying assembly code they use Z mod 2^32 for arithmetic right?
<KipIngram>
siraben: Your Forth has no return stack? Or do you just mean that it's not user accessible?
<siraben>
KipIngram: oh I was talking about when I will specify and formally verify a language that compiles to a stack VM, it will have while loops, assignment, arithmetic expressions, but no procedures
<remexre>
siraben: yeah, it'll probably be my PhD thesis once I actually get around to it, lol
<siraben>
KipIngram: in my Forth I have the whole shebang, return stack and all
<remexre>
I think the SAIL people do Z mod 2^n, yeah
<KipIngram>
:-)
<siraben>
remexre: that'll be cool, a PhD made by a formally verified Forth!
<KipIngram>
I kind of feel like having the return stack exposed is more or less required to claim the name "Forth."
<siraben>
Forth makes it ideal in some ways, I know the compcert (formally verified C compiler) folks had such trouble with the C spec being imprecise and undefined
<remexre>
yeah, and being able to tweak the semantics if it makes verification easier helps a lot too :)
<remexre>
I'm sorta expecting it to be a pain that I have a max stack size, though hopefully I can write some ltac to just automate that? (if I'm using Coq that is; I'm considering Abella since I probably don't need too many metalogicy things?)
<siraben>
yeah I wonder what to do with max stack size
<siraben>
i'll let it be infinite first then maybe prove that "if the program uses at most N items on the stack, a stack size of N will allow it to terminate"
<siraben>
similar to how "if the program has enough gas, it will terminate with correct result" as in the IMP chapter in logical foundations
<siraben>
remexre: another minor difficulty is microcontrollers have finite memory, so you might want to do address arithmetic modulo the size
<remexre>
well, I've got virtual memory anyway, since I run at EL1
<siraben>
EL1?
<remexre>
ring0 in x86 terms?
<siraben>
ah I see, I wasn't familiar
<remexre>
yeah, arm does EL0 = userspace, EL1 = kernel, EL2 = hypervisor, EL3 = secure firmware thingy
<siraben>
I think it's a great project, there needs to be more intermediate-advanced material like it
f-a has quit [Read error: Connection reset by peer]
f-a has joined #forth
gravicappa has quit [Ping timeout: 240 seconds]
<DKordic>
siraben: That worked. Thank You.
f-a has quit [Ping timeout: 240 seconds]
f-a has joined #forth
andrei-n has quit [Quit: Leaving]
<KipIngram>
remexre: What software are you running that has those rings?
mtsd has quit [Ping timeout: 245 seconds]
<remexre>
my forth runs at EL1, since I'm writing an OS in it
<KipIngram>
Oh, that's nice. So you're writing all the device drivers and so on yourself?
<remexre>
yep
<KipIngram>
That's fantastic - what machine does it run on?
<remexre>
though, good odds I won't be supporting anything other than virtio and a basic serial driver for a while
<remexre>
right now just qemu, though with some tweaking I can boot it on the rk3399
<KipIngram>
Where did you find documentation on all the boot-up details?
<KipIngram>
Decades ago I could all of that in bookstores, but I don't know where to find it now.
<remexre>
partly the arm manual, partly experimentation, partly the sources of {u-boot,qemu,linux}
<KipIngram>
There used to be a LOT of nice "low-level" books.
<KipIngram>
I'm very impressed. That's the kind of thing I'd love to do someday but just have never found the time.
<KipIngram>
Multi-core?
<remexre>
nope, though I'm going for an IPC-heavy microkernel design, so it shouldn't be "that hard" -- I'd just designate a special area for cross-cpu IPC, and run one copy of the kernel per core
<KipIngram>
Definitely update us now and again - I look really forward to watching you bring that up. :-)
<KipIngram>
I eventually want to push my Forth to bare metal, but for now it uses a handful of MacOS syscalls to interact with the hardware. I emulate disk blocks in a big "blocks.dat" file.
<KipIngram>
So I'm working on "everything else," and then someday I'll have a clean, well-defined (and small) set of words that I'll need to re-write to deal with actual hardware.
<remexre>
oh, nice; yeah, I'm probably emulating blocks too, but probably only supporting nvme at first (allegedly it's really simple?)
<KipIngram>
You know, I should know that, because our SSDs present NVMe to the host. I think I've got a copy of the spec around somewhere - do you have that?
<KipIngram>
Anyway, I'm very very excited about your project - I'm sure I can learn some good stuff from you over time.
<remexre>
hopefully I can teach you useful stuff then lol; I'm not really a super-expert on this stuff either though
<KipIngram>
Well, maybe we can figure some of it out together. Just the fact that you're doing this encourages me to perhaps give it a go.
tech_exorcist has quit [Quit: tech_exorcist]
tech_exorcist has joined #forth
tech_exorcist has quit [Ping timeout: 252 seconds]
<KipIngram>
I have two major goals for mine "on the other end." I'm adding an extra formal layer to the system - I'm implementing the primitives using a set of macros that I call "portable instructions." I haven't done it perfectly yet; a few times I've been chasing a bug and just wanted to get the code in. But I'll go back and fix that at some point. The idea is that the only thing I should have to port to move the
<KipIngram>
system to ARM is those macros. So that's one goal. The other is to eventually migrate all of the source into the system itself and have it able to rebuild itself.
<KipIngram>
Part of the reason I wanted that portable instruction layer is that I tend to write very primitive-heavy systems. I want the best possible performance, so I do a lot more as primitives than I absolutely have to. So I just don't want that to be the porting layer.
Zarutian_HTC has quit [Read error: Connection reset by peer]
Zarutian_HTC has joined #forth
<KipIngram>
The idea behind the macro layer is that it generates more or less optimal primitives, at least on x64 and ARM.
<KipIngram>
I haven't even started an ARM version yet.