> People always get upset when I propose mathematical formalization of law and using e.g. metamath verifier as a judge.
I don’t get upset. I just don’t know what that means. What would that look like in practice?
Lets see some simple example. 18 U.S. Code § 912: “Whoever falsely assumes or pretends to be an officer or employee acting under the authority of the United States or any department, agency or officer thereof, and acts as such, or in such pretended character demands or obtains any money, paper, document, or thing of value, shall be fined under this title or imprisoned not more than three years, or both.”
How would you write that in mathematical formalization?
And then how would you make a metamath verifier judge if Robert J. Rippee committed it on
January 1, 1991? I’m sure you can google the case(United States v. Rippee, 961 F.2d 677), but a short summary: “On January 1, 1991, officers from the National City, Illinois, Police Department stopped Rippee for making an illegal U-turn. The officers let Rippee go without a ticket, however, when he told them he was a United States Marshal on his way to break up a fight at Fannies' Night Club in Brooklyn, Illinois. […] Rippee stipulated that he was not and had never been a United States Marshal.“
How would something like that look like under your proposed system?
> I don’t get upset. I just don’t know what that means.
metamath is an open source formal verification system, the current metamath project (not focussed on law, but mathematics) has roughly 3 parts:
1) the formal verifier (there are multiple re implementations)
2) the databases of axioms (including definitions), theorems and proofs: currently most math is in set.mm the database for set theory (which includes numbers, etc)
3) documentation, among which a thorough book describing how the formal verifier works, the book is creative commons
A proof is basically a series of invocations (by label) of axioms, or previously concluded facts or rules, in the right order so that the verifier comes to the desired conclusion. The algorithm performs all the substitutions and after the last invocation either the string it arrived at matches the proclaimed theorem or it doesn't. Of course it can also error out earlier, say if an invocation to an unknown label happened.
Precisely because natural language is ambiguous, the conversion of our natural laws into formal ones would have to happen under democratic control.
If academic mathematicians want to preserve a human mathematical academy in the face of governments potentially making the future mistake of abolishing mathematical academia, their strong move would be for them to define a "government for and by mathematicians", the database would contain definitions of their choosing, formally regulating how to award public funds into research, formalizing front-running resistant timestamping of work-in-progress etc, so that mathematicians can freely talk and communicate advances ("just wait a sec, let me sync my insights with the network first, ... aaand done, ok now I can speak freely").
Ultimately from a survival perspective, which type of system do we believe to be more robust against corruption and conflicts of interest? one where due process is formally defined in a rigorous manner? or one where those who corrupt the system happen to corrupt it towards actual progress?
Can you walk through the process for the proposed example?
The problem in most suites is checking if a specific act in real life meets some definition of a crime and not figuring out the wording of the law, right?
You kill someone without a reasonable excuse -> You get punished x years for murder
wouldn't really make murder trials easier because you would still have to formalize what you put into the proof.
> I’ve often wondered why governments don’t provide a ‘dating’ service for employers and employees, or even better some kind of career development and management service for citizens.
Don’t they? Here in the UK at least participation in programs like that is a requirement of unemployment benefits. One has to attend a job center where one is given advice, sometimes training can get enrolled in trainung and etc. Not saying that they do a great job of it but they seems to at least try to do what you describe. At least nominally.
I would never design a robot which looks like it can walk, but actually can’t walk. That feels fundamentally dishonest to me. If nothing else it will let down plenty of people when they realise that the cool robot has legs only for show.
Fair point, the legs can give that impression, but JBR-001 is made as and announced as a desktop companion, legs are there for support and appearance, but it doesnt walk. This is the first version, design files are open source and we would love to see someone build a version that does walk.
But it is the fuselage gaps which was leaking, not the engines. After the elastomer filler broke down due to heat cycling. They needed the elastomer because the fuselage was heating up during flight which made it expand.
I'm sure we could "fix" it. But changing the engines doesn't seem to be the right way to achieve that.
It is not even clear from the article that there were anything wrong with the output. She has a car of that make. And it doesnt appear to be in dispute that she drove nearby.
It simply is the case that “being nearby” in itself is not enough evidence that you were involved in a crash. Especially when the colour doesn’t match and the vehicle is not damaged.
The fundamental problem here is that the police are very bad about false positives. Flock gives them a ton of data--but that doesn't make it magically perfect. No surprise there was a similar car nearby--there are a lot of similar cars. Flock shows them the similar cars and they pick the closest without any investigation.
It looks cool! But man is it frustrating that nothing is consistent. Some things change when I click. Some things change when I drag. Some things seemingly doesn't do anything at all.
If it is intentionally like that, great. But I just don't find the experience pleasant.
Backstory: when we first set up the sandbox, we offered a handful inputs that devs could optionally use in their letters. You could click and drag directly on the letter, drag a little token on a "Kaoss Pad"-like control surface, scrub a timeline, toggle a big global mode switch, and more. Everyone used a different subset of the these inputs, based on whatever seemed like the best fit for the idea behind their letter. Some people even bypassed all that and implemented their own input handling (like Lilith did for the bullet hell game in C0). But most folks actually didn't add any interactivity at all.
When I curated the letters for our home page, I wanted to strike a balance between a few things. I wanted to encourage playfulness, for instance by having unpredictable things happen depending on what/how you interacted ("output randomness", to borrow a gamedev term). And while I did make some changes to some letters (adding some additional interactivity, simplifying some inputs), I didn't want to go too far and ruin the authorial intent behind the letters.
But, like you and the other commenter here found, there is inconsistency that errs on the side of frustrating. That's something that irked me too — I just ran out of time for polish and had to ship.
In any event, thanks for kicking the tires on it. Even if it didn't quite clear the bar for playful interaction, I hope it was fun to look at.
I don’t really mind the inconsistencies, it is just something fun and playful to discover and I believe the imperfections add to the charme of such things. It reminds me of the little sketches I made with Processing[1] years ago, when programming felt like just another artistic medium I could express myself in.
Just wanted to say that I personally enjoyed the little inconsistencies. It feels satisfying to discover interactions that I didn't expect, disorienting but in a good way.
> There will hopefully (?) come a time one day when human beings provide only ultimate value judgments, and everything else is done by machines.
In their previous grandparent post. They do reserve a place for human value judgement, but I doubt even that remains if everything else has been automated. The machines will decide what we value. We already see that to some degree with algorithmic engagement and targeted advertisements.
The (?) is meant to express doubt that it is a good thing on net. But regardless of whether it is, it is what is likely to happen, and there will certainly be some good things that come out of it.
> It’s stuck in the auto calibration stage. It gets halfway through then it stops with a generic error message.
So it was dead on arrival. You should have contacted support who would have figured out if you need the whole unit replaced or just part of it. If they are not responsive enough just send back the whole thing.
What would you do if you buy a laptop and it never passes the Power-On Self-Test? I would just return it to whoever i bought it from.
> I thought it was the more turn key option but it hasn’t been my experience.
I mean it is. For everyone who i know who owns one. Every company will sell an occasional dud.
Either it got damaged in transit, or the fault somehow escaped their QA, or you managed to screw up the assembly by not plugging in something, or leaving a transit fixture in somehow. Either way contacting support is the correct way to get to the bottom of it.
Come to think of it when i bought my Sherline lathe initially the motor didn’t turn on when i plugged it in. I wrote an email to the distributor who got me in contact with someone from Sherline. They asked me to check a thing which fixed the issue.
> So it was dead on arrival. You should have contacted support who would have figured out if you need the whole unit replaced or just part of it.
I mentioned that in my comment. I contacted CS. Multiple times in fact. They wanted to diagnose the issue remotely before issuing a refund. Their instructions were poorly written and assumed familiarity with the internals of the machine. ChatGPT helped some but not completely. Then life got busy, I had work travel and the 30 return window passed before I realized it.
Your response is, frankly, a little condescending. You seem convinced this is somehow my fault or that sat there twiddling my thumbs. Of course I understand that duds make it through manufacturing at times. It’s great that the happy path is easy. Do we judge the accessibility of a product only by how it behaves when everything goes right? I was careful during assembly and watched multiple YouTube videos and read the official instructions when putting it together, I contacted CS. In retrospect I should have pushed harder for a refund, but my original point still stands. As someone who wanted a “just works” solution, what I got instead was something faulty and then a really painful process for getting it solved.
It's condescending because there is not much to it.
Like, if the Bambu Labs printer doesn't work either you did nothing wrong and it is broken or you did something incredibly stupid. There is no in-between where e.g. knowing how to build your own Voron gives you an edge in fixing it yourself.
It sounds equally condescending to say that it is difficult to set up a Bambu Labs printer when what you are doing is actually full on fault diagnostics of the internals which you shouldn't have to do. You're allowed to complain about DOA products and terrible QA processes or bad customer support.
Obviously customer support has a perverse incentive to shift the blame onto the customer because RMAs are expensive so you got caught in the crossfire of a defective printer and the customer support.
> They wanted to diagnose the issue remotely before issuing a refund.
They were stalling you. You are in someone’s succesfull quarterly KPI metric, as a succesfully avoided return.
> You seem convinced this is somehow my fault
That the printer is not working is 100% Bambu’s fault. That they got away with it is yours.
> As someone who wanted a “just works” solution, what I got instead was something faulty
So there is a misunderstanding here. When people describe a 3d printer as “just works” they mean that it has the sensors and firmware smarts so you don’t need to become an expert to get good quality prints out of it. With previous generations of printers when the print was crap you had to look at the process and tune a ton of parameters to get it okay. Maybe your bed wasn’t flat enough? Or hot enough? Or unevenly heated? Or you needed to tweek an extrusion parameter? Or speed it up or slow it down? Or increase the hot end temp? Or increase the cooling fan rpm?
With a modern 3d printer (like the Bambu ones, but not only them) you don’t have to become an expert. Their engineers nailed down all the parameters which can be nailed down, and the rest which they can’t they added sensors for so the printer can measure them as an in-field calibration.
With the older generation of printers if it is not printing well, oh boy, you should probably get better at tuning it. With the new generation of printers if it is not printing well then the company who made the printer failed you. If it is not printing at all, because it failed the calibration then that’s the printer telling you it is broken.
It is like… imagine that you want a nice picture of your loved ones. Buying an older type of printer was like buying oil paint and a brush. You can’t just hope it will do the picture on its own. You could get the picture you wanted but you had to acquire serious skills first. No art supply shop would accept a return of your paint and brush just because the picture you paint with it are kinda crap.
In contrast buying a new generation of 3d printer is like buying a polaroid camera. It requires way less skill than the oil paint and the brush. You point, you shoot, out comes the picture. If the picture doesn’t come out the polaroid camera is broken and you should return it.
The polaroid camera is “just works” compared to the oil paint and brush even if every second camera is broken comming out of the factory. Because it is not a statement about their defect rate, but a statement about the design philosophy.
I'm not sure what you are hoping from "free", "community owned", and "open source".
They make mills and lathes. They are really nice little machines, great for hobby use. We have one lathe from them in our hackspace for example, and it is a delight. Of course you have to understand the limitations of the tool, but that is true for every machine.
That being said, it is just a lathe. There is nothing particularly complicated about it. At least not at their complexity level. If you can manufacture machine tools you can make one very easily. If you don't have the manufacturing capability you won't.
The reason i'm saying this is because "free as in freedom" and "open source" are properties of plans / source code. If you happen to have a lathe factory, the lack of a lathe plan is not going to stop you. You are just going to design one for yourself. And if you don't have a factory which can make a lathe, then why do you care about plans for a lathe being open source?
I guess the factory itself could be "community owned". If you have a business plan, or a large pile of cash, now is the time to approach them that you want to buy everything from them. But I'm not sure how "community owned" would even work for this use case.
Basically what I'm saying this is hardware, not software. The terms you use don't make much sense in this case.
> They were not around long enough to confirm whether or not it happened for days
And that is perfectly fair. But what is the “possibly days” based on? Did they see the two whales acting weirdly a day later, but then they didn’t see them four days later? Or is it just based on the hunch of the person who made the observation? Or is it the hunch of the researcher? And if it is a hunch is it based on knowledge of similar reported events in the past? Is it based on the observed state of the adult whale or maybe the state of the carcas?
Why possibly days and not possibly weeks?
> but the fact that the mother stayed for at least some hours appears to be confirmed
Is it confirmed? So that’s the problem. The hours are comming from the same sentence which describes the days. Both by a person who did not whitness the event personally. Your reading is that the second part of the sentence (the days) is speculation, while the first is reporting on observed fact. My reading is that the journalist did a bad job separating the first hand observed facts from the second hand speculation. We just simply won’t know until someone asks the Captain what exactly they have seen and writes it down.
> it’s hard to know and prove something with 100% certainty
But it is not hard to describe what was observed, and clearly separate it from what they think or speculate. Also it is not hard to ask the person who actually did the observing to describe what they have seen, instead of it being described by someone else who was not present.
You are correct. The underlying scientific article is clear on the timeline of observations. My problem is with the editing done by the phys.org article.
I don’t get upset. I just don’t know what that means. What would that look like in practice?
Lets see some simple example. 18 U.S. Code § 912: “Whoever falsely assumes or pretends to be an officer or employee acting under the authority of the United States or any department, agency or officer thereof, and acts as such, or in such pretended character demands or obtains any money, paper, document, or thing of value, shall be fined under this title or imprisoned not more than three years, or both.”
How would you write that in mathematical formalization?
And then how would you make a metamath verifier judge if Robert J. Rippee committed it on January 1, 1991? I’m sure you can google the case(United States v. Rippee, 961 F.2d 677), but a short summary: “On January 1, 1991, officers from the National City, Illinois, Police Department stopped Rippee for making an illegal U-turn. The officers let Rippee go without a ticket, however, when he told them he was a United States Marshal on his way to break up a fight at Fannies' Night Club in Brooklyn, Illinois. […] Rippee stipulated that he was not and had never been a United States Marshal.“
How would something like that look like under your proposed system?
reply