109000+ entries in 0.065s
a111: Logged on 2018-04-12 20:55 asciilifeform: spyked: in re proof machines, i'm much moar interested in items like ACL2 , where you can affix your hand-written program
to a hand-written proof of correctness in a mechanically-reliable way
a111: Logged on 2014-02-26 14:52 mircea_popescu:
they let it run overnight, among
the conclusions it had arrived
to by morning was "napoleon had an infinite number of arms"
a111: Logged on 2018-04-12 20:48 asciilifeform: spyked: if you recall, back in
the 'minsky age',
that was
the initial attraction of mechanical 'reasoners' -- discovery of ~simple~ inferences
mircea_popescu: btw, does it occur
to anyone else
that #trilema is way ahead of i dunno, black-chicks-code or whatever other imperial nonsense in
terms of both headcount, volume or value of female participation in
techgeneering ?
a111: Logged on 2018-04-12 19:42 avgjoe: no, it's a easy/fake study
to have more spare
time keeping government grants
mircea_popescu: zx2c4 specifically for
the "empty room" problem he brought up. do you follow
the logic
there ?
trinque: kittycollector and sashahsas, you used
the same address. someone is lazy.
lobbes: technical design aside
though,
there's still
that obvious fact
that we have
to rely on various $mtgoxes for market price :/
Though I'm not sure what be a better source for a fiat-btc exchange rate (iirc
this was a mini-thread somewhere in logs)
lobbes: Then I have Process B
that is
triggered on changes
to
that database doing
the various "market price" retrieval and volume averaging. Process B inserts retrieved data into database and Process A responds accordingly
lobbes: been
thinking
through
tickerbot design, and seems like
the sane
thing would be
to have Process A (which is an instance of logbot-genesis with "logbot-multiple-channels-corrected" patch) running
that makes changes
to a postgresql database.
a111: Logged on 2018-04-12 20:20 spyked: zx2c4, I've been looking over
the
tamarin protocol verification paper and I'm curious, what does "symbolic verification" mean? also, what's
the
thing's output? is it just a "yes, properties hold" or does it also output
the proof?
zx2c4: spyked:
http://btcbase.org/log/2018-04-12#1797801 tamarin (and cryptoverif and proverif) spit out
the proof
too.
tamarin has a nice mode
that will draw diagrams and flow charts
too
to make it easier
to digest
the proofs. people even have scripts
to convert
the output into latex in case you want an academic paper for free...
☝︎☟︎ a111: Logged on 2018-04-12 18:00 asciilifeform: it resembles 'nano ecc' which at 1 point asciilifeform
tried
to port
to
trb
a111: Logged on 2018-04-12 07:03
trinque will get
to
these
tomorrow, girls
a111: Logged on 2018-04-12 20:55 asciilifeform: ada's spark is a similar, if somewhat uglier/bulkier,
thing
ben_vulpes: yeah i can't
this
thread anymore,
too damn seductive.
ben_vulpes: bang gas is
then a pressure-drop
triggered combustion?
mimisbrunnr: Logged on 2018-03-23 04:08 douchebag: Okay, why do you guys liek arguing so much? Is
this why you guys don't get anything done?
ben_vulpes: i
think it puts
the water in
the wrong place. you get dry, hot air which you'd
then have
to cool and compress into
the engine and cold wet air (possibly with
the water condensed out entirely with a spigot)
jurov: you want it
to separate water, no?
ben_vulpes: you get some gases
that speed up, pulling energy out of
the gases
that slow down which dump energy into
the higher speed gases. not purely a 'sorter'.
jurov: but i don't know if same
temperature means h2o and o2 molecules have same momentum? or
they have same kkinetic energy?
jurov: i
think
the vortex sorts particles by momentum, not necessarily by
temperature
☟︎ ben_vulpes: you'll want
to compress it somewhat for reasons of efficiency; consider again
the diesel and its
turbo
ben_vulpes: heh well
then you gotta cool
the dryer, dontcha
ben_vulpes: asciilifeform: yeah here and
there, more frequently we simply flooded
the workpiece with coolant.
ben_vulpes: might work if you had enough expander and volume
to slow
the intake down and get it out of
the incompressible regime
ben_vulpes: "The Use of
the Expansion of Gases in a Centrifugal Field as Cooling Process"
ben_vulpes: there is an expander in
the diagram, had a sign error
ben_vulpes: it'll cool, sure, but nowhere near as much as if it were a gas, as
the gas will condense and pull further heat out of
the local system.
ben_vulpes: just cribbing from wikipedia here, but "there is no longer cooling observed since cooling requires compressibility of
the working fluid"
ben_vulpes: refrigeration depends on compressibility of
the working fluid
ben_vulpes: my first q is what is
the breadth of intake gas velocities and fluxes
that such a device could handle
a111: Logged on 2018-04-12 20:10
trinque: a muntzed drakma would be a fine
thing, I'd sign
spyked: more
to
the point,
this is similar
to asciilifeform's "auditability" question. is
there a way
to obtain a (ideally human-readable) set of deductions out of
the prover?
spyked: zx2c4, I've been looking over
the
tamarin protocol verification paper and I'm curious, what does "symbolic verification" mean? also, what's
the
thing's output? is it just a "yes, properties hold" or does it also output
the proof?
☟︎ trinque: a muntzed drakma would be a fine
thing, I'd sign
☟︎ spyked: whole
thing's a mess, but I'm organizing
the code so
that I can eventually replace it with something else.
spyked: okay
then, I'm gonna work it off
this. it'd be enough
to replace
the "drakma"
http client with something lighter, and I'd already cut about half of it.
the dependency
tree leads
to
two xml parser libraries being used (plus other redundant stuff).
trinque: nope, current
thing is a sad pythonball hanging off
the side.