Man, I have lost my voice on this issue. Disagree and commit they say.
I'll tell you, managing two systems in different languages that need to interoperate, it's tough. I'm so sad C/C++ couldn't get organized and iterate towards something better. There is a huge trade-off being made here - all the effort spent writing some things in Rust, well it's also not going to fixing all the C++ code. That's still there. Sometimes the forest gotta burn for new flowers to bloom. I hope it burns fast.
Right, the bang per syllable loss is it's ambiguous, not that it's incorrect. Inverse square root could also mean -(x^0.5) if it meant the additive inverse, and it could mean x^2 if it meant the functional inverse, as said here.
The point would be to prove that your database stays consistent, a DB upgrade wouldn't break, or that you could achieve 100% up time given certain assumptions. An automated solver/prover might even be able to tell you where in your program breaks this. Without a technology like this, you have to carefully read your program, but this is the methodology to make the computer deal with that. Unfortunately formal verification is mostly used for research, F* is framing itself as taking a step to bring that to production codebases. Unfortunately I don't know good resources, but as researchers adapt this technology, and as we automate a lot of the heavy mathematics, you'd never want a programming language without this option.
F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. In Coq, there's not a standard way to generate code, you might model and create code many different ways. F* seems to bring this in as the central goal of the language. So I'm discussing this structural difference. F* has an SMT solver, but Lean can import an SMT solver. So the goal is the important difference here - making theorem proving as accessible as possible in a real language. It's a move in the right direction, but we want to get to the point standard program languages have this support if you need it.
I studied formal languages for ~2 years and have professional experience programming coq. The real benefit of this language, over other formal languages is the focus on being able to write real programs in it. Most theorem proving languages are focused on mathematics or proving things about a program, and they are very abstract. This language appears to have a goal of bridging the gap and making it simple to write programs and prove parts of them. I believe this is the future of formal languages. If you write something in Rust, it would be great to prove aspects about it. Why not? Well F* is a vision if this future. As proof automation gets better, we will be able to prove many things about our programs, something which is not typically attempted due to difficulty. For instance, imagine proving that a certain path has no allocations, spawns no threads, cannot deadlock, preserves privacy, only modifies a certain subset of global data, is a specific algorithmic complexity, is not subject to timing attacks, maintains the conference of a cache, is memory safe (without a borrow checker). The limit is your imagination and Rice's theorem.
A student who believes in the freedom of information and is curious probably will do great in school. A great institution understands rules are meant to uplift and protect us, and that a student who sees beyond black ink and chiseled stone for a better tomorrow is the very same breed of rule maker which creates such great institutions in the first place. I know first hand from colleagues, bypassing the censorship is common for intelligent youth in China. We must always ask ourselves what the best is we can do and always avoid the "dangerous slippery slopes"
I don't think this is the distinction being made here. Abstractions may be useful framing, but the author contrasts, after hearing what addition is, are you going to start studying multiplication, or are you going to look at examples of addition. We'd never think about teaching a child multiplication before they know their addition tables. However, in higher level math, and I saw this in uni, it's common to study structures without knowing many examples of them. You can do proofs about groups without connecting any of these proofs to actual examples that show their utility.
As someone reading this while taking a shower, I'm questioning how this could be redesigned to work today. How are you supposed to use your phone if your head is sticking out?
You can always find disagreement if you look for it. Maybe this is your thing, given user name, your account makes an interesting study on it. Though in this case, I wouldn't be so reductive. Not all complexity (I ascribe to the result) is due to bad intentions (e.g. greed). There's also the EU GDPR trying to protect kids. AI assistant might be a tool to try to help users. If you want to simplify the cause here, how about a lack of focus or failure to tame the complexity of the world with our technologies, or tendency to add rather than delete?
So many pop-ups these days, for every little thing. Tracking. OS permissions. Browser permissions. Take a survey. Speak to our AI assistant. Do you agree to this. Donate. Sign up. Pay. So many clicks. Used to be viruses, but we have the same result with our complexity.
There are a few examples of repeated testing being used by alignment groups to either test how aligned a model is, or to aggregate results to get something that is more aligned. For instance this is one related discussion: https://artium.ai/insights/taming-the-unpredictable-how-cont...
The non-determinism is a feature, and it can be disabled. This article also mentions doing that to get more deterministic alignment tests.
Theoretically if you aggregate enough results, it might become improbable to ever see an unaligned output. However, from a practical standpoint, we clearly much prefer much smarter models than running dumber models in parallel to get alignment that way. It's inefficient. The other thing is that given the number of possible ways to jailbreak a model, you can probably find something that would still bypass ensemble-based protections.
One other concept is relativism - there is a large grey area here. What is okay for someone is not okay for someone else, so even getting consensus among people what is okay, it's just not going to happen.
Fun read, thanks! I really like redefining terms to break LLMs. If you tell it an LLM is an autonomous machine, or instructions are recommendations, or that <insert explicitive> means something else now, it can think it's following the rules, but it's not. I don't think this is a solvable problem. I think we need to adapt and be distrustful of the output.
The issue your parent comment raises is that this random group may not represent someone that's trying to evaluate what techniques can help them, regardless of the statistical significance within that group. It makes me sad that they introduce other random variables, as incontrovertible evidence of efficacy could help a lot of people!
Lol. Even if it's with the QR code, it will not be safe. If you can read a bit, you can read a file. Security is a mote, and the hacker is a catapult. Any sufficiently complex system, any metric of security will be incomplete or ignoring that Turning complete and uncomputable. Security is about intelligence in all layers of the stack, from the electron to the application and even the front door. A USB exploit attacks a driver or the OS. A QR code attacks the application. There are other ways to exploit besides breaking and entering. Sometimes it's about influence. In the age of AI, the entire internet and all knowledge could be shifted to reframe a single organization to make an exploit possible. Pandora's box is wide open. It's pouring out. Even a machine on the internet can be secure, but an air gap is only the transport layer. It's a false sense of security. You need to be worried about the full stack because that's the only way to be safe, to never be safe, the eternal guard and gaze. The vigilance. Security in layers. Security in depth.