daly

Your linked article claims it was not a lab leak.

re: BSL-2 vs BSL-4 ... Assuming it WAS a lab leak, was there an a-priori reason to believe that among the many different naturally occurring viruses under study that SARS-CoV-2 would cause a worldwide pandemic? Bats are known to have hundreds of different viruses. Ebola and HIV seem to have been spread widely without a lab connection.

As for gain-of-function studies, they might be beneficial. One might, for example, modify a DNA-modifying virus to add a gene for expressing insulin, providing a cure for diabetes. A DNA-modifying virus provides an ideal whole-body carrier for genetic disorder correction. Indeed this hackernews post (https://news.ycombinator.com/item?id=40307138) today shows a deaf girl cured through genetic manipulation. See https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4786910/

Lab leak?

Vincent Racaniello, a leading virologist (https://www.microbe.tv/twiv/) seems to think that the genetic sequence of the covid virus and the bat version of the virus are nearly identical. That genetic evidence seems to suggest that the covid virus had a natural bat source.

Vincent talks about and shows safety practices for a "level 4 biolab" (https://www.bu.edu/articles/2013/video-offers-glimpse-of-bio...)

It might be the case that the biolab safety protocols were not followed. This seems unlikely.

It might be the case that there was a cross-species transfer of the virus. This is a frequent event between species.

Scientifically, a lab leak is less likely than a species-transfer. Politically, a lab leak is the only possible (i.e. politically useful) explanation.

So your sources of information comes from a world-leading virologist and a state department spokesperson.

You decide.

Motivated by this post I found my oldest laptop. It still boots. During boot it displays "memory counting" ... up to 256k! It runs DOS from diskettes. Ah, memories :-)

I've been looking at yeast to see if it is possible to create a NOR gate. Then the game is to use the CPU that someone created in Conway's game of life to create a yeast-based computer.

The CRISPR stuff:

"We demonstrate the world’s first successful editing of the human genome using a gene editing system where every component is fully designed by AI. Our most performant AI-generated editor, OpenCRISPR-1, achieves similar activity and higher specificity than SpCas9, an exemplar gene editor, while being highly dissimilar in sequence. Moreover, our platform is capable of generating many more gene editing systems at-will; OpenCRISPR-1 is just the tip of the iceberg. We publicly release OpenCRISPR-1 to facilitate broad, ethical usage across research and commercial applications. In making this molecule available to the broader community, we hope to lower the costs and barrier to entry for therapeutic, agricultural, and scientific applications of CRISPR-based technologies." https://www.profluent.bio/blog/editing-the-human-genome-with...

Conway's Game of Life CPU: https://www.youtube.com/watch?v=Kk2MH9O4pXY&ab_channel=AlanZ...

Yeast-based NOR gate: https://www.nature.com/articles/ncomms15459

I've finished one textbook on yeast so far. I've looked at doing CRISPR at home: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC9053061/

There is an ongoing effort on "yeast evolution" to create new kinds of yeast behavior https://www.ncbi.nlm.nih.gov/pmc/articles/PMC9225242/ and, in particular, yeast seem to self-specialize when, through "directed evolution" they start to cooperate https://www.sciencedirect.com/science/article/pii/S200103702...

There already is known machinery to do switching in cells: https://www.amazon.com/Genetic-Switch-Third-Lambda-Revisited...

This form of epigenetics allows all kinds of interesting responses to external stimuli. In particular, it would allow "chemical questions" to be asked.

It would be possible to create a cellular "display":

"Scientists from Trinity College Dublin, in collaboration with the Royal College of Surgeons in Ireland (RCSI), have developed special fluorescent, color-changing dyes that, for the first time, can be used to simultaneously visualize multiple distinct biological environments using only one singular dye.

When these dyes are encapsulated in delivery vessels, like those used in technologies like the COVID-19 vaccines, they “switch on” and give out light via a process called “aggregation-induced emission” (AIE). Soon after delivery into the cells their light “switches off” before “switching on” again once the cells shuttle the dyes into cellular lipid droplets."

So when your Petri dish "yogurt" "sees you" open the fridge it can change the surface to say "Hello". Coming to a fridge near you...

I suspect it gives more weight to "a gut feeling" when your stomach can argue for a viewpoint in actual words. We'll leave off the question of how to avoid angry mutterings from your toilet :-)

I have about 6000 books, about 1000 of these are on Kindle.

Of the 6000, most have bookmarks. I read at least the first 50 pages of most of them. I've finished a couple hundred so far. I found my old business cards make perfect bookmarks.

I guess "No one buys books" isn't strictly true.

I tried to write 4 books. I was told that I'd likely sell less that 1000. Beyond that would be considered a major win. I finished one, published it, and have made about $500. It took me months to write.

I love books. I have a copy of "I, Robot" signed by Asimov. I really like books signed by authors.

The engine intakes will be blocked by the body in high angle of attack.

I've spent my life trying to understand computers, all the way from the chemistry of the quality of quartz used to make wafers up to the nuances of LLMs and their robot embodiments.

I'm a level 1 kinda guy. I never quite understood people at other levels. Do you want to do computers because other people do (level 2), because you have a better gaming computer (level 3), or you love Apple products? (level 4)

This is a really insightful article. It explains why everyone is "into computers" but don't want to discuss transistor dielectric breakdown or high-bandwidth memory or functional programming or ...

We need names for the levels such as Deadhead (level 1), Groupie (level 2), Fanboy (level 3) and Comicon (level 4).

Methinks the attempt to create general purpose quantum computers is a false direction.

Once you've played with a quantum computer (I used IBM's online QC) the novelty wears off. It is basically "operators" (2x2 Pauli matrices,etc).

The key problems seems to be that the quantum lifetime is very short and by the very nature of quantum computation it requires multiple runs to get statistics.

It is my opinion that there ought to be a list of "quantum solvable questions". Then there ought to be a focus on creating fixed-purpose quantum solutions.

For example, the problem of understanding particular chemical bonds to improve something like high/low friction surfaces. Build a fixed-purpose quantum computer that optimizes those computations.

I'm pretty sure the chemists could create a list of questions they would like answered.

This would create a market for companies that specialize in building fixed-purpose machines that solve real problems.

In other words, "build-to-purpose" rather than "build-for-anything".

There is a huge market for first-movers in build-to-purpose.

Love to play with it but not at that price. It's going to cost me a LOT of time and attention, wasting time with installing drivers, setting up the whole dev environment, deciding if the bug is mine or theirs, etc.

Not to mention that it is RISCV. I have half a dozen RISCV board so I'm already familiar with the processor. I've even created on softcore RISCV on my FPGA. But I'm pretty sure I'm going to spend a lot of time trying to cross-compile software for this Grayskull Dev Kit.

I can buy a low-end NVIDIA GPU for about $200 and it will "just work".

Traditional AI approaches to games involves reinforcement learning (RL). This type of learning is also used post-LLM as reinforcement learning with human feedback (RLHF) to improve the LLM.

At the moment my effort involves a focus on mathematical proofs using this technology.

RL requires a few things. It requires a notion of 'states'. It requires 'actions' that can be applied within states. It requires a success/fail measure, either when moving from state to state or only at the end of an effort.

Now consider mathematical proofs.

The LEAN project[0] has developed an IDE[1] that guides proofs, It guides the user "from state to state" keeping track of the current state.

There is a database of axioms and theorems[2]. Each of these are strongly typed so they can only be applied in specific states.

There are "tactics" which are actions from state to state.

Success can be found when the proof is successful. Intermediate success can be measured by recording what tactics / axioms / theorems were applied.

The use of strong types means that there are only a few actions that apply in each state. Traditional arguments about exponential growth limiting brute force no longer apply.

SO ... we now have all of the elements of a game. Which means that we can apply reinforcement learning to LEAN proofs. I suspect that "proving theorems" will be one of the next areas overtaken by AI.

[0] http://www.contrib.andrew.cmu.edu/~avigad/Papers/lean_system...

[1] https://en.wikipedia.org/wiki/Lean_(proof_assistant)

[2] https://www.andrew.cmu.edu/user/avigad/Talks/mathematical_co...

I spent hours in the tower trying to mimic the controller's flight instructions, approach, landing, taxi, takeoff, departure, and flight following.

It is an impossible job. I multitask really well but the controllers are just absolutely talented. Write a little program that randomly generates tail numbers and actions then try to keep it all straight. One mistake and somebody might die.

Suppose you weigh 180.0 lbs. Suppose your target weight is 160.0

Week 1 at 180.0. Eat ONLY when you weigh less.

Week 2 at 179.9. Eat ONLY when you weigh less.

Week 3 at 179.8. Eat ONLY when you weigh less.

...

You get the pattern.

When you eat you can eat anything you want.

When you reach your target weight eat ONLY when you weigh less.

You could probably do the same thing with bacterio-rhodopsin. I used it to build a form of rewriteable paper. It switches states based on two different laser frequencies.

I worked on an early 1970s computer with out-of-order processing. I got an interrupt due to a faulty instruction which caused a core-dump (aka a huge pile of paper containing a memory printout delivered by a very angry machine room operator). The message was that the failure occurred sometime in the last 16 instructions... which could have been branches from anywhere.

The only effective debugging technique was omphaloskepsis.

Sigh.

Tesla chargers use a fluid in the charging hose to handle heat buildup. The chargers in question got too cold and the fluid froze to the charger stopped working. Tesla needs to change the fluid formula for colder weather.

The press got it all wrong. It had nothing to do with batteries.

I worked with Nqthm and ACL2. They seem best adapted to hardware verification.

LEAN is pushing the edge of undergrad mathematics.

Thanks for the "all the work" complement. Despite all, it is more fun than work.

Computer algebra algorithms are basically functions. Axiom is unique in that it organizes the functions based on a group theory scaffold. Thus you can know that certain matrices commute but rectangular ones don't. Algorithms that know how to commute live in the commutative "category" in Axiom. So the game is to distribute LEAN's commutative axioms in their proper place in the group theory inheritance scaffold so they are available when they apply.

Axiom arranges the world into "categories" (not category theory stuff) and "domains". The LEAN structure is a third structure (actually fourth but...) built in parallel so that a theorem that proves that certain matrices commute will only be available when it applies. When you try to prove your algorithm you have a collection of LEAN axioms, definitions, and tactics that are valid and apply to your particular function. If your algorithm used rectangular matrices the commutative theorems would not be visible and thus not available in a proof step. Due to the hierarchical nature, once you prove an algorithm you can also use it in other downstream proofs, for example, using proven data structures and their properties.

I have not published any papers on the subject. I'm no longer anywhere in the academic pipeline so a paper wouldn't get very far. Plus this is "in the cracks" kind of research that doesn't seem to fit into either camp.

As for the education or research question... I'm trying to do what I call "computational mathematics". It would have "real world impact" for Proof Systems so they would be able to depend on and use proven computer algebra results. Computer algebra systems would benefit by giving proven answers. Both areas would benefit.

Don't try to build a computer algebra system from scratch. Axiom has hundreds of years of PhD level research work embedded in its code. There is no way to reproduce some of it as the people have died. Researching just one of the algorithms could take the equivalent of a PhD effort. I tried to introduce literate programming so that people could learn to maintain, modify, and extend Axiom. The idea is that you could "read the docs" and both learn from the authors and have embedded pointers to the theory literature. Without literate programming I believe that the whole effort will eventually die as the learning curve is very steep. Literate programming was an attempt to keep Axiom "alive". Nobody wanted it. I gave a talk on it once: https://www.youtube.com/watch?v=Av0PQDVTP4A&ab_channel=NextD...

There is no "team". There is just me. Apparently I'm bad at "team". I have no desire to get forked again.

Having experience with prior open source work I'm not likely to release the current effort until I'm much closer to completion. The whole idea of CAS and Proof has already generated a hostile reception from both areas in my email stream.

I've already proven that if I did release Axiom again I'm too socially inept to manage the process anyway. I'd release a technical paper or two but I'm no longer associated with CMU so I'm pretty much a "hobby researcher" I guess. The last Axiom presentation was the invited talk at Notre Dame prior to Covid.

There are a lot of interesting things "in the works" though. One is the idea of "proof down to the metal" (aka Proof Carrying Code[0]). The use of (FPGA) field programmable gate arrays[1] and the RISC-V[2] architecture soft-implemented in the FPGA means that I can run the LEAN proof in parallel with the algorithm at the hardware level. This not only proves the algorithm correct, it proves the implementation correct. I have a few FPGAs.

It's all fun and games but I have to wait to release it.

[0] https://en.wikipedia.org/wiki/Proof-carrying_code

[1] https://en.wikipedia.org/wiki/Field-programmable_gate_array

[2] https://en.wikipedia.org/wiki/RISC-V

Tim Daly here...

There were quite a few challenges before Axiom could be open sourced.

NAG released the Axiom sources to me around that time. I gave an invited talk in Paris.

There were many issues to solve. The primary one was that you needed a running Axiom to build Axiom. I was not allowed to distribute the NAG version of a running Axiom. It took a long time to restructure the system so it could be built from sources.

Portions of the NAG version were never distributed to me and I had to recreate some from scratch.

GNU hosting and Sourceforge hosting were new technologies I had to master. I also struggled to understand how to create and lead an open source effort. Obviously in hindsight I'm very bad at management.

The NAG version of the system removed the Common Lisp version of AKCL, (of which I'm a minor author). AKCL is now GNU GCL under Camm. IBM Research sponsored the creation of AKCL under contract which was developed by Bill Schelter. Bill and I were in constant contact and he used my office on his site visits. I had to re-host Axiom on AKCL from the NAG version but Bill was dead by then.

Back then I was working at City College of New York in the CAISS effort involving Infinite Group Theory (Magnus). I maintained, modified, and extended that effort and made it open source. Axiom was not part of my job effort until the last few months of my time there. Axiom was all after-hours / off-the-clock work. (I see my name has been "scrubbed" from the CAISS/Magnus work. They even mention Axiom but not me. Sigh.)

Axiom is now exploring new research ideas combining computer algebra and proof theory (aka computational mathematics). The computer algebra people don't do proofs and the proof people don't do computer algebra algorithms. In fact, of the few hundred papers I reviewed only James Davenport made the bibliography section in both areas. I'm not expecting any enthusiasm for this research. If I fail no one will notice. If I succeed ... no one will notice :-) But I'm having fun.

Tim Daly here...

Axiom is alive, well, and under active development. The current effort is merging the LEAN [0] proof technology with the Axiom algebra. This involves some deep restructuring. The target result is proven algorithms, something missing in current CAS work.

(Note that this is project goal F on http://axiom-developer.org)

The effort involves building a parallel architecture to the current Axiom category / domain layout to enable functions to use LEAN's axioms, definitions, and tactics to prove existing algorithms.

In addition, Axiom now uses Common Lisp CLOS to enable work using dependent types, something not currently available in the legacy system. The algebra hierarchy is now a CLOS hierarchy which enables a lot of flexible extensions.

There is no point in publishing the work as open source since it is still in the active research phase. When released it will be announced on the http://axiom-developer.org website and uploaded to github.

One of the Axiom algorithms (Groebner basis[1]) has been proven in Coq.

Wikipedia contains the literate form of Axiom[2] , including the original book restored from the NAG files.

There is an active fork maintaining the legacy code as mentioned above.

[0] The LEAN Theorem Prover https://www.andrew.cmu.edu/user/avigad/Papers/lean_system.pd...

[1] Bruno Buchberger. Bruno buchberger’s phd thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Journal of Symbolic ComputationVolume 41, Issues 3-4, Logic, Mathematics and Computer Science: Interactions in honor of Bruno Buchberger (60th birthday),, 2006.

[2] Wikipedia Axiom https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system...

I have walked with coffee cups all my life. Coffee is almost my only drink. The only time I've spilled coffee was if someone bumped me or I bumped something. I've been doing it for over 60 years. One must not waste the elixir of life.

Here's a suggestion for Oxford... Only fill the cup half way. Or, rather than cut down on your carrying capacity of vital fluids you can change your natural frequency... learn to walk with a limp :-)

I have about 2000 hours of flight simulator time starting from when it first came out. I really miss Meigs field.

I signed up for private pilot lessons.

The first day with the instructor I did a walk around inspection, started the plane, talked to the tower, did a taxi and takeoff.

The instructor let me fly for a while then put me "under the hood" so I couldn't see, said "It's my airplane", took control and flipped it all around, and then said "Your plane". The flight controls were all I could see. I could see that I was in a dive with rotation so I cut the throttle, centered the stick and kicked opposite rudder until the rotation stopped then regained level flight.

The flight instructor said that was "pretty good but could be better". I asked him if this was a first-day test for a private pilot's license. He was shocked. He thought I was going for an instrument rating. I pointed out that this was my first time ever in a small plane and first time ever as an actual pilot.

The lessons got easier after that :-)

So, yeah, if you spend a year's worth of time in the sim it will help a lot.

Nuke plants gradually deteriorate due to the neutron flux which causes atomic displacements in atoms. This is a particular problem in the containment vessel. Forty years of intense bombardment weakens the structure.

I taught COBOL while at grad school at UCONN. Methinks I'm getting old.

Cybertruck Superfan here...

This whole essay is nonsense. The high demand implies a higher price (economics 101). Tesla is right to keep the price high until volume production kicks in.

As for range. 340 miles is sufficient for most tasks involving trucks. It is also in range of most of the electric trucks (and most other trucks in that category).

I won't bore you with the list of features.

The Cybertruck is stunning. I want one. I want one NOW.

It would be amusing to have a conversation between ELIZA and GPT.

It is certainly true that the parent can do both jobs. However the spawn is a much smaller model that can be in a smaller machine.

My dad, Joseph J. Daly, was a civilian employee of the Coast Guard at the statioin near Wildwood Crest, N.J.

Dad built, tested, and deployed a lot of the Loran transmitters. He delivered one to Iwo Jima during the second flag raising.

Dad also took a trip in a van with Loran equipment. The van drove up the Garden State Parkway so they could measure the accuracy.

He and I talked a lot about high-Q notch filters, used to handle local stray electromagnetic problems. We also talked a lot about temperature control for clock stability.

Many years later I happened to meet the Coast Guard guy whose job it was to shut down Loran.

The Crowd: A Study Of The Popular Mind by Gustave Le Bon

https://www.files.ethz.ch/isn/125518/1414_LeBon.pdf

AAA study finds ADAS could save more than 8000 lives per year

https://youtu.be/UVfDrivSm58?t=754