--- Log opened Tue Jul 01 00:00:28 2025
00:10 < fenn> @Eli who is spending nearly $10k on AI diagnosis as shown in your MAI-DxO pareto frontier image? and how? what are they even doing with that many tokens?
00:10 < fenn> or is the cost to pay a human to read the output?
00:46 -!- flyback [~flyback@2601:540:c700:2380:5dc7:706a:c1b7:69e9] has quit [Ping timeout: 276 seconds]
00:59 -!- flyback [~flyback@2601:540:c700:2380:979b:b30:f803:c312] has joined #hplusroadmap
01:55 < fenn> ah it's the cost of diagnostic tests
01:57 < fenn> "Clinicians in our study worked without access to colleagues, textbooks, or even generative AI" seems like a bad control group methodology
03:01 -!- TMM [hp@amanda.tmm.cx] has quit [Quit: https://quassel-irc.org - Chat comfortably. Anywhere.]
03:01 -!- TMM [hp@amanda.tmm.cx] has joined #hplusroadmap
03:32 -!- darsie [~darsie@84-113-82-174.cable.dynamic.surfer.at] has quit [Quit: Avoid fossil fuels and animal products. Have no/fewer children. Protest, elect sane politicians. Invest ecologically.]
03:33 -!- darsie [~darsie@84-113-82-174.cable.dynamic.surfer.at] has joined #hplusroadmap
04:08 -!- gl00ten [~gl00ten@194.117.18.99] has joined #hplusroadmap
04:08 -!- gl00ten [~gl00ten@194.117.18.99] has quit [Remote host closed the connection]
05:32 < hprmbridge> kanzure> "Another one… a big wishlist one. An enzyme that unwinds a target protein in vivo and ligates trinucleotides together based on which amino acids are in the peptide chain. I.e. a reverse ribosome. yes I've seen reports of people working on ClpX-based systems that use antibodies specific for amino acid motifs to recognise the peptide sequence as it is unwound. AI-guided structural design of small
05:32 < hprmbridge> kanzure> binding proteins might soon be able to give us proteins that act as the 'inverse-tRNAs' - they bind to a free amino acid in a linear peptide chain and pull in a DNA (or RNA) tag that then ligates to a growing nucleotide read out." (reverse translation) https://x.com/ProfTomEllis/status/1940016094695047430
05:36 < L29Ah> https://www.youtube.com/watch?v=ncfZWqPm7-4
05:37 < fenn> could i interest you in a nanopore
05:37 < hprmbridge> kanzure> bacteria published some open-source electrowetting stuff a long time ago
05:37 < fenn> hackteria
05:37 < hprmbridge> kanzure> uh, hacktrfia
05:37 < hprmbridge> kanzure> ffffff
05:38 < hprmbridge> kanzure> there are several proposals for reverse translation of proteins into nucleic acids available in the patent literature
05:41 < hprmbridge> kanzure> huh, none of which I can find at the moment
05:45 < kanzure> https://patents.google.com/patent/US20070087377A1/en
05:45 < kanzure> https://encodia.com/
05:49 < kanzure> https://glyphic.bio/
05:49 < kanzure> https://www.quantum-si.com/
05:49 < kanzure> https://41j.com/blog/2021/07/dreampore-nanopore-protein-sequencing/
05:57 < kanzure> kent has this crazy idea (being kent almost all of his ideas are completely nuts) about using a basic selection experiment design to find a sequence of nucleic acids that causes conversion of sunlight into oils?
06:00 -!- L29Ah [~L29Ah@wikipedia/L29Ah] has quit [Ping timeout: 276 seconds]
06:01 < kanzure> what's nice about cells and nucleic acids is that they are extremely tiny objects, and they have high "material bandwidth" (i dunno what to call) it since it is executing in the real physics environment
06:04 < kanzure> the following link contains a high amount of bullshit word vomit but is ostensibly about gradual brain tissue replacement as a longevity or survival strategy https://danburonline.substack.com/p/death-is-an-engineering-challenge?open=false#%C2%A7approach-ectopic-cognitive-preservation
06:05 < kanzure> "progressive tissue replacement" rather
06:06 < kanzure> "progressively composed of the new graft material integrated with embedded electronics" not sure how this works. in aubrey's version of this, you inject stem cells 'liberally', non-surgically and not site-specifically. so where you putting those electronics and why?
06:07 < kanzure> i also don't understand how danny burgers is getting from "progressive tissue replacement" -> "ex vivo brain perfusion" or if that is supposed to be a decoupled idea.
06:15 < kanzure> for progressive tissue replacement in human brains, a neat trick would be to somehow preserve long-range axons or dendritic trees (in a reusable way) even if you are lesioning a specific area. possibly a space-filling intracellular parasite.
06:23 < kanzure> "We want to make biochemistry as intuitive to program as computer code. No more stochastic events. The bio-engineer should simply look at the molecule and tell it what to do. We're building controllable nanomachines that let bioengineers see and control single molecules in real time, in situ and in vivo. Our nanomachines are protein/enzyme-based and can be [conformationally] controlled with ...
06:23 < kanzure> ...lasers to do a bunch of chemical work." kakamatech@gmail.com
06:31 < kanzure> "The whole neuron project: I'm trying to create a molecular map of a neuron. Like, litterally reconstruct every molecule (proteins, RNA, lipids, ions, etc.) with spatial context, either by direct data or smart prediction"
06:35 -!- L29Ah [~L29Ah@wikipedia/L29Ah] has joined #hplusroadmap
06:36 < L29Ah> https://bmcbiotechnol.biomedcentral.com/articles/10.1186/s12896-018-0439-9
06:38 < L29Ah> https://www.researchgate.net/figure/The-Mondrian-microfluidic-cartridge-a-Image-of-the-cartridge-b-Diagram-of-the_fig6_325517600
06:39 < kanzure> L29Ah: curl https://diyhpl.us/~bryan/papers2/microfluidics/ | grep lectrowet
06:49 < kanzure> tom ellis says "Fun fact - in 2009 I was supposed to go work for Mark Chee’s tech dev start-up that Glyphic spun out of but California ran out of H visas so I just applied to academic jobs in the UK as a back up plan. Great to see they are getting there now with this idea." this does not sound like a fun fact.
06:51 < kanzure> oops he meant encodia not glyphic 
06:51 < L29Ah> call your congresscritter today
08:11 -!- TMM [hp@amanda.tmm.cx] has quit [Quit: https://quassel-irc.org - Chat comfortably. Anywhere.]
08:11 -!- TMM [hp@amanda.tmm.cx] has joined #hplusroadmap
08:20 < L29Ah> may i interest you with a cyberpunk techno opera? https://mind-in-a-box.bandcamp.com/album/memories
08:31 < hprmbridge> Eli> Probably most of the planet doesn't have any doctors. That's why there will be demand. So, it's not that it will need to start here. And it could have difficulty here because of legal and regulatory issues. But, if it starts being used in places where people are too poor to have doctors, it could end up being difficult for Westerners to see that and not demand the same thing. Because there are
08:31 < hprmbridge> Eli> many Westerners who can't afford doctors either. And even people who have doctors are misdiagnosed a lot. That's why none of the elites use government healthcare in any developed country.
08:34 -!- darsie [~darsie@84-113-82-174.cable.dynamic.surfer.at] has quit [Quit: Avoid fossil fuels and animal products. Have no/fewer children. Protest, elect sane politicians. Invest ecologically.]
08:35 -!- darsie [~darsie@84-113-82-174.cable.dynamic.surfer.at] has joined #hplusroadmap
09:13 < kanzure> who here is a formal verification wizard?
09:14 -!- geneh2 [~cam@pool-71-191-180-23.washdc.fios.verizon.net] has joined #hplusroadmap
09:15 < geneh2> interesting project from DARPA on controlling chemistry with spin, not sure what became of it https://www.darpa.mil/research/programs/spin-controlled-chemical-process-engineering
09:15  * L29Ah is just a haskell type system fanboy
09:17 < kanzure> https://hacspec.org/
09:36 < kanzure> "aerosolized H5N1 by combinatorial genome engineering and in vivo selection" https://youtu.be/MHR0K45q-8k 
09:36 < TMA> kanzure: wannabe formal verification wizard, not quite there yet
09:36 < kanzure> TMA: how far are you
09:36 < TMA> at the start
09:37 < kanzure> codeshark really wants a formal verification project for bitcoin
09:37 < TMA> I think I know the required logic, but I have not yet wrapped my head around the tools at all.
09:37 < kanzure> there are several ways to slice this problem. partly the issue is that the reference implementation is, essentially, the specification. so the current behavior according to C++ definition, and any undefined behavior, must be captured.
09:38 < TMA> ouchies
09:38 < kanzure> this is slightly different from the typical formal verification task (specification -> proofs about that specification)
09:39 < kanzure> kcc / K Framework supposedly has an ability to emit information about undefined behavior or other semantics, for gcc/clang; the execution trace produced by K is a formal model of the program; you can symbolically execute it or export it as logical constraints.
09:40 < kanzure> CBMC gives a 'formal' intermediate representation or program (SMT/Boogie/CHC); ESBMC has C++ STL stuff so that's nice...
09:40 < TMA> I have read a presentation of doing a subset of plain C in TLA+. The thing expands like crazy. Even really small things blow up
09:40 < TMA> really fast
09:41 < kanzure> "SMACK is an automated software verifier, verifying assertions given in its input LLVM intermediate representation (IR) programs. Under the hood, SMACK is a translator from the LLVM IR into the Boogie intermediate verification language (IVL). Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract ...
09:41 < kanzure> ...interpretation"
09:41 < kanzure> https://github.com/smackers/smack
09:44 < kanzure> it is plausible to write a formal spec anyway, even if it is not generated by analysis of C++
09:44 < kanzure> although whether it would be correct would be in question
09:48 < TMA> formal specification of bitcoin blockchain, consensus, protocol, ...
09:48 < TMA> do I understand the requirement correctly?
09:51 < TMA> so formal specification of cryptographic primitives is a "subspec" of the whole?
09:51 < kanzure> mainly the consensus rules, obviously things like GUI components in Bitcoin Core are not of interest for these purposes
09:54 < TMA> I don't think I am advanced enough just yet. I cannot even estimate how much work that would be.
09:56 < TMA> it could be "we could have a high level model in few months" or "in 2060 we could be done with the preliminary exploration" I cannot tell at the moment
09:59 < kanzure> it's not clear to me what the goal even would be; if you have a specification, then you want to be able to make proofs about that specification. but that is not the situation.
10:01 < kanzure> instead of a specification, you have an implementation. and you maybe want to generate a specification from that implementation? but why not just use the actual build artifact and run that?
10:03 < kanzure> codeshark is specifically requesting "A public, rigorous specification that is neutral, formally verifiable, and allows other people to write and verify their own implementations"
10:12 < andytoshi> kanzure: C++ is not formally defined and even if it was it's extremely unlikely that gcc meets that formal spec
10:13 < kanzure> yeah..... sure.
10:13 < kanzure> honestly i think something that is not "formal verification" would meet his goals
10:13 < andytoshi> a subset of C is formally defined, by compcert, and they have a compiler that meets the spec, and maybe-probably gcc meets the spec on that subset, for popular processors, because C is very simple
10:13 < kanzure> for example, why not "just use the bitcoin core test suite" a suitable answer for "how can i verify if my implementation is compatible"?
10:13 < andytoshi> because a test suite cannot capture anything except a tiny space of possible behaviors
10:14 < andytoshi> and you cannot even usefully describe that tiny space to identify gaps
10:15 < kanzure> the traditional answer here is that the bitcoin implementation is the spec itself
10:15 < kanzure> so why not just fuzz over the interface/domain and sample as much as you are willing to expend on compute costs? for checking cross-implementation compatibility i mean.
10:16 < kanzure> possibly you would need a new way to specify how to fuzz at this semantically higher level, and how to prioritize the search space
10:17 < andytoshi> sure, you should do that. but "fuzz as much as you are willing to spend on compute costs" does not remotely resemble what a formal spec would get you
10:18 < andytoshi> it's unlikely even to reveal a single new consensus behavior that nobody knows about
10:18 < andytoshi> even though there are definitely many left
10:18 < kanzure> so.... i'm not saying this is a good idea or that it meets the actual strict definitions of formal verification.
10:18 < kanzure> my goal is maybe some sort of proposal to satisfy the demand ("A public, rigorous specification that is neutral, formally verifiable, and allows other people to write and verify their own implementations")
10:19 < kanzure> and we are allowed to relax 'formal verification' there because there are serious questions about what that even means in this context or whether it is even possible in the true definition of the word in the field of study.
10:19 < andytoshi> it is not possible to satisfy that demand, even in the weaker sense that you wrote it
10:19 < kanzure> haha interesting
10:19 < kanzure> i mean it depends on what "verify" means
10:20 < andytoshi> it is not possible to specify the script interpreter well enough to allow other implementations, unless you first softfork in a reduced-functionality subset tof script which can be formally defined
10:20 < kanzure> to be fair we do not have a rigorous proof that bitcoin core is itself bitcoin-bitcoin compatible with itself, for even the same version
10:20 < andytoshi> which is probably a good idea, but won't happen for political reasons
10:21 < kanzure> so when i see the word 'verify' yes formal verify would be nice but at minimum the acceptable definition of verify is whatever level of testing is in the core tree test suite
10:21 < andytoshi> i can't imagine that is "acceptable" for anybody who is requesting something more than the existing test suite
10:22 < andytoshi> or who wants something actionable
10:22 < kanzure> well, what is the intention of the request, right? the intention is something about "let other people write software and verify it". anyone can already write software. now what is verify? we can't even verify bitcoin core conforms to bitcoin core at the moment.
10:23 < andytoshi> the intention is that people be able to write other consensus impls without consensus bugs in them
10:23 < kanzure> that's the correct thing to do, if we were capable of doing it; but there are strong arguments that we cannot. how is "use the test suite" worse than doing nothing?
10:24 < andytoshi> it's not worse. it's just not better :)
10:25 < kanzure> a more fundamental issue here is that it will not achieve codeshark's goals (political peace)-- but i'm ignoring this aspect.
10:26 < kanzure> andytoshi: do you know ~things about the core test suite? does anyone run huge matrixes of core versions against each other across ~200 CPUs etc? i haven't seen this spoken about.
10:27 < kanzure> it's a combinatorial explody problem
10:27 < kanzure> ~200 different CPUs is what i mean
10:28 < kanzure> something like not assuming strict substrate equivalency between versions of core and versions/types of hardware substrate to run it
10:28 < andytoshi> you can run the core test suite on your own computer in like 5 minutes
10:28 < kanzure> (and likewise for network configurations)
10:28 < andytoshi> if you have 200 CPUs you should run the fuzz tests
10:28 < kanzure> no
10:28 < kanzure> not what i mean
10:28 < kanzure> it is very common in commercial software projects to test commercial software in a CI/CD platform across many different operating systems and hardware substrates (like different brands of CPUs)
10:29 < andytoshi> yes, and the bitcoin core CI runs the test suite in that way
10:29 < kanzure> and, in network-related software projects, it is common to do some level of combinatorial testing (different previous versions against new versions on a mix of different hardware)
10:29 < kanzure> yeah but i am curious about depth of test coverage
10:29 < kanzure> er, hardware coverage is more accurate for my last line sorry
11:41 < jrayhawk> i used to live with formal a verification toolchain guy; AFAICR the recommended approach is to incrementally move as much of functions into a dependent-type language such as Idris as possible and centralize impurity and non-terminating behavior into the smallest possible core
11:41 < jrayhawk> er, with a formal
11:52 < kanzure> that makes you the most qualified so far!
12:55 < kanzure> oh nevermind
12:55 < kanzure> pmetzger has roflstomped your qualifications
13:08 < jrayhawk> if you're actually serious about it, your HEB backend friend whose name escapes me can refer you to a bunch of Galois and Galois-adjacent folks who live, eat, and breathe this stuff.
13:32 < jrayhawk> jblake would probably also know some people
14:25 -!- darsie [~darsie@84-113-82-174.cable.dynamic.surfer.at] has quit [Ping timeout: 252 seconds]
14:52 -!- L29Ah [~L29Ah@wikipedia/L29Ah] has left #hplusroadmap [Disconnected: closed]
14:58 -!- L29Ah [~L29Ah@wikipedia/L29Ah] has joined #hplusroadmap
15:48 -!- stipa_ [~stipa@user/stipa] has joined #hplusroadmap
15:51 -!- stipa [~stipa@user/stipa] has quit [Ping timeout: 252 seconds]
15:51 -!- stipa_ is now known as stipa
15:54 -!- Mabel [~Malvolio@idlerpg/player/Malvolio] has joined #hplusroadmap
16:08 < hprmbridge> Katylase> hi friends! how are you doing?
16:10 < L29Ah> wondering whether there's a meaningful limit to infill fractalization for part rigidity per weight optimization
16:12 < hprmbridge> Katylase> infill? are you 3d printing something?
16:13 < L29Ah> yes
16:13 < L29Ah> ever heard of sandwich panels?
16:13 < hprmbridge> Katylase> no?
16:16 < hprmbridge> Katylase> also, can I ask you something?
16:18 < L29Ah> never ask to ask
16:19 < hprmbridge> Katylase> oki! so, do you know Foldit?
16:21 < L29Ah> i played it a bit long time ago
16:21 < L29Ah> was pissed that it is buggy and closed source
16:21 < L29Ah> and today alphafold probably made it obsolete
16:23 < hprmbridge> Katylase> actually, it isn't buggy now... and has integrated alphafold fitting
16:25 < hprmbridge> Katylase> and! since it's the only game about proteins I know, I decided to make my own...
16:26 < hprmbridge> Katylase> (I'm obsessed with them^^)
16:29 < hprmbridge> Katylase> when you played it, did it still have radial menus?
16:30 < hprmbridge> Katylase> like this? https://cdn.discordapp.com/attachments/1064664282450628710/1389749979928858764/IMG_3417.webp?ex=6865c107&is=68646f87&hm=a354b01dfef7a687d07d84aa2c4844a9447309079964d27804dcc7c14a9a2292&
18:34 < hprmbridge> kanzure> we have a foldit world champion in here
18:35 < hprmbridge> kanzure> separately does anyone have good ideas for how to verify a user's IQ or ethnicity online, without requiring government intervention?
18:39 < L29Ah> build an organization that does it offline and gives certificates
18:40 < L29Ah> see also: worldcoin
18:46 < hprmbridge> kanzure> ugh worldcoin
18:46 < hprmbridge> kanzure> but even then, I don't think they capture that data
18:50 < L29Ah> i don't mean use worldcoin, i mean you can look up their experience in building a similar organization
18:50 < L29Ah> there's also stuff like IELTS
18:50 < hprmbridge> kanzure> the eyeball scan hash stuff?
18:51 < hprmbridge> kanzure> and HSM eye scanner orbs?
18:51 < hprmbridge> kanzure> the trouble is that it requires a trusted root org to deploy "secure" hardware
18:51 < L29Ah> people usually use meatware for that
18:52 < hprmbridge> kanzure> online that won't work due to deepfakery
18:52 < L29Ah> just tolerate some degree of error due to faulty meat and corruption
18:52 < L29Ah> again, you must do it offline
18:52 < hprmbridge> kanzure> maybe p2p assertions Web of Trust
18:53 < hprmbridge> kanzure> and 23andme verification via trusted central server?
18:54 < L29Ah> and it also depends on your attack vector
18:55 < L29Ah> Sybil comes to mind at first, then you have the problem of IQ tests being trainable
18:55 < hprmbridge> kanzure> well you can do IQ polygenic scoring, but the data collection for polygenic data becomes attackable over time
18:55 < L29Ah> so what are you trying to protect against? SJW activists trying to ruin your research?
18:56 < hprmbridge> kanzure> eh just interested in weird online community experiments
18:56 < hprmbridge> kanzure> eg US only, 100 IQ only, Canadian only etc
19:01 < L29Ah> scientific publications very often use questionnaires and static tests for such, with no verification except maybe outlier pruning, because it is hard and they need to be producing science yesterday; do you need the verification through increasing your costs a couple orders of magnitude over that?
20:02 -!- flyback [~flyback@2601:540:c700:2380:979b:b30:f803:c312] has quit [Quit: Leaving]
20:10 -!- flyback [~flyback@2601:540:c700:2380:d038:b30b:40f4:61ed] has joined #hplusroadmap
20:24 -!- justanotheruser [~justanoth@gateway/tor-sasl/justanotheruser] has quit [Ping timeout: 244 seconds]
20:28 -!- justanotheruser [~justanoth@gateway/tor-sasl/justanotheruser] has joined #hplusroadmap
21:09 < hprmbridge> Eli> I feel like I saw a link on here about how people were replacing CAPTCHAs with basic calculus problems to screen out normies?
21:34 < superkuh> The easiest is to self-sign HTTPS.
22:15 -!- darsie [~darsie@84-113-82-174.cable.dynamic.surfer.at] has joined #hplusroadmap
23:41 -!- TMM [hp@amanda.tmm.cx] has quit [Quit: https://quassel-irc.org - Chat comfortably. Anywhere.]
23:41 -!- TMM [hp@amanda.tmm.cx] has joined #hplusroadmap
--- Log closed Wed Jul 02 00:00:29 2025