thesmtsolver (u/thesmtsolver)

thesmtsolver commented on Coq: The World's Best Macro Assembler? (2013) [pdf] nickbenton.name/coqasm.pd... · Posted by u/addaon

kragen · 2 months ago

I'm curious about how you'd do that, too. I haven't tried doing anything like that, but I'd think you'd start by trying to formalize the usual optimality proof for the Kalman filter, transfer it to actual program logic on the assumption that the program manipulates real numbers, try to get the proof to work on floating-point numbers, and finally extract the program from the proof to run it.

https://youtu.be/_LjN3UclYzU has a different attempt to formalize Kalman filters which I think we can all agree was not a successful formalization.

thesmtsolver · 2 months ago

It is really not that difficult. Here is a paper that formalizes a version of feed forward networks to prove properties about them.

https://arxiv.org/pdf/2304.10558

thesmtsolver commented on Coq: The World's Best Macro Assembler? (2013) [pdf] nickbenton.name/coqasm.pd... · Posted by u/addaon

quanto · 2 months ago

> when I can get away with it I'd prefer to prove things with real numbers and assume magically they transfer to floating point.

True for some approaches, but numerical analysis does account for machine epsilon and truncation errors.

I am aware that Inria works with Coq as your link shows. However, the link itself does not answer my question. As a concrete example, how would you prove an implementation of a Kalman filter is correct?

thesmtsolver · 2 months ago

There is nothing inherently difficult about practical implementations of continuous numbers for automated reasoning compared to more discrete mathematical structures. They are handleable by standard FOL itself.

See ACL2's support for floating point arithmetic.

https://www.cs.utexas.edu/~moore/publications/double-float.p...

SMT solvers also support real number theories:

https://shemesh.larc.nasa.gov/fm/papers/nfm2019-draft.pdf

Z3 also supports real theories:

https://smt-lib.org/theories-Reals.shtml

thesmtsolver commented on AI isn't replacing jobs. AI spending is fastcompany.com/91435192/... · Posted by u/felineflock

echelon · 3 months ago

This is the biggest unspoken story in tech.

The era of American developer exceptionalism is over.

Talent abroad has access to the same tools, education, and increasingly, network. American engineers will be replaced wholesale with overseas engineers that cost a fraction of American labor.

You can hire talented React engineers for $50k that will work harder than their American counterparts.

It's not just React. Overseas markets have DevOps, SREs, embedded, systems engineers, you name it.

For years Americans joked that overseas labor was subpar. It's not, or at least it isn't in today's world.

thesmtsolver · 3 months ago

Any data backing this? If this were the case, why isn’t most innovation done outside the US?

Jobs that have a high 0-1 component will still be in the US but jobs that are more 1-n may be offshored.

thesmtsolver commented on Kimi K2 Thinking, a SOTA open-source trillion-parameter reasoning model moonshotai.github.io/Kimi... · Posted by u/nekofneko

MallocVoidstar · 3 months ago

> What we’re going to see is as energy becomes a problem

This is much more likely to be an issue in the US than in China. https://fortune.com/2025/08/14/data-centers-china-grid-us-in...

thesmtsolver · 3 months ago

Disagree. Part of the reason China produces more power (and pollution) is due to China manufacturing for the US.

https://www.brookings.edu/articles/how-do-china-and-america-...

The source for China's energy is more fragile than that of the US.

> Coal is by far China’s largest energy source, while the United States has a more balanced energy system, running on roughly one-third oil, one-third natural gas, and one-third other sources, including coal, nuclear, hydroelectricity, and other renewables.

Also, China's GDP is a bit less inefficient in terms of power used per unit of GDP. China relies on coal and imports.

> However, China uses roughly 20% more energy per unit of GDP than the United States.

Remember, China still suffers from blackouts due to manufacturing demand not matching supply. The fortune article seems like a fluff piece.

https://www.npr.org/2021/10/01/1042209223/why-covid-is-affec...

https://www.bbc.com/news/business-58733193

thesmtsolver commented on Tech workers' fight for living wages and a 32-hour workweek is a battle for all thechiefleader.com/storie... · Posted by u/robtherobber

bee_rider · 3 months ago

I wonder if there could ever be a tariff policy that is automatically proportional some measure of worker/environmental exploitation. I know tariffs are current very unpopular, but maybe they can be used for good?

thesmtsolver · 3 months ago

That will be a great solution. Tariffs based on some measure of worker/environmental exploitation rather than trade imbalance.

thesmtsolver commented on Tech workers' fight for living wages and a 32-hour workweek is a battle for all thechiefleader.com/storie... · Posted by u/robtherobber

esafak · 3 months ago

Countries can stay ahead by enticing better workers with better working conditions. I ain't doing 996.

thesmtsolver · 3 months ago

> I ain't doing 996.

Neither am I. But how do you prevent countries doing 996 from dominating the market like they did in manufacturing without strict regulation and barriers?

thesmtsolver commented on Tech workers' fight for living wages and a 32-hour workweek is a battle for all thechiefleader.com/storie... · Posted by u/robtherobber

thesmtsolver · 3 months ago

How does this work with other countries not enacting 32-hour workweeks?

This will be a repeat of manufacturing going outside of US due to reduced standards (labor and pollution) and therefore cheaper manufacturing in China. And due to that blue collar work got destroyed in the long term.

Logically, unless there are high trade barriers for software/services/goods from countries that don't have similar standards, long-term, these jobs will just shift there.

thesmtsolver commented on US will not send officials to COP30 climate talks reuters.com/sustainabilit... · Posted by u/geox

thesmtsolver · 3 months ago

I feel these agreements are highly asymmetric and are used to gain market advantage by countries that don't have qualms violating these agreements behind closed doors.

This then leads to more pollution.

Before Trump, the US had a higher rating than China (though both were bad):

https://climateactiontracker.org/countries/usa/2024-11-13/

(Same as EU's rating: https://climateactiontracker.org/countries/eu/)

https://climateactiontracker.org/countries/china/2024-09-17/

The sad reality is that unless there is uniform compliance across major countries, these talks are just climate theatre.

thesmtsolver commented on Attention lapses due to sleep deprivation due to flushing fluid from brain news.mit.edu/2025/your-br... · Posted by u/gmays

wslh · 3 months ago

It is always great to follow the instructions from a psychiatrist [1].

[1] https://thelastpsychiatrist.com/2007/08/how_to_take_ritalin_...

thesmtsolver · 3 months ago

This is just outdated, bad and dangerous advice that a ton of recent research invalidates.

1. Ritalin, and other stimulants are not cognition enhancing for non-ADHD adults and may in fact do the opposite.

https://www.cam.ac.uk/research/news/smart-drugs-can-decrease...

2. > Because the doctor will rigorously apply artificial and unreliable diagnostic categories backed up by invalid and arbitrary screens and queries to make a diagnosis. So after this completely subjective and near useless evaluation is completed, your doctor should be able to exercise prudent clinical judgment to decide if Ritalin could be of benefit.

What else can you do for psychiatric conditions? We don't have a magic ADHD-o-meter but know that it statistically impacts lifespan, health, etc. Even for more objective measures like blood glucose, BP, BMI, clinical interventions are based on discrete thresholds that don't exist in nature.