In a lot of my AI assisted writing, the prompt is an order of magnitude larger than the output.
Prompt: here are 5 websites, 3 articles I wrote, 7 semi-relevant markdown notes, the invitation for the lecture I'm giving, a description of the intended audience, and my personal plan and outline.
Output: draft of a lecture
And then the review, the iteration, feedback loops.
The result is thoroughly a collaboration between me and AI. I am confident that this is getting me past writer blocks, and is helping me build better arcs in my writing and lectures.
The result is also thoroughly what I want to say. If I'm unhappy with parts, then I add more input material, iterate further.
I assure you that I spend hours preparing a 10_min pitch. With AI.
Great example. Just give me the links you would give to the LLM. I also have an LLM and can use it if I want to, or I can read the links and notes. But I have zero interest in reading or hearing a lecture that you yourself find too tedious to write.
You have less interest in sifting through multiple articles and wiki pages sent to you by a stranger with a prompt than the one paragraph same stranger selected as their curated point.
And pretending like you’d act otherwise is precisely the kind of “anti ai virtue signaling” that serves as a negative mind virus.
AI is full of hype, but the delusion and head in sand reactions are worse by a mile
No pretending here. I don't ever ask an LLM for a summary of something which I then send to people, because I have more respect for my co-workers than that. Nor do I want their (almost certainly inaccurate) LLM summary. It's the 2020s equivalent of "let me Google that for you": I can ask the bag of words to weigh in myself; if I'm asking a person it's because I want that person's thoughts.
Then let him curate it as his central point. If he finds even that too tedious to do, I absolutely have no interest in reading the output of a program he fed the context to (particularly since I also have access to that program)
The code lets you shoot yourself in the foot in a lot more ways than a spec does, though. Few people would make specs that include buffer overflows or SQL injection.
I can only say that at family meetings, I hear people talk about contracting with a shop that used to have 4 web designers, but now it's 1 guy, delivering 4x faster than before.
Uhm, no?
Even with "simple" examples like Dijkstra's shortest path, the spec is easier than the implementation. Maybe not for you, but try it out on an arbitrary 5-yr old.
On the extreme end, you have results in maths, like Fermat's Last Theorem. Every teenager can understand the statement (certainly after 10 mins of explanation) but the proof is thousands of pages of super-specialized maths.
It is a spectrum. For cryptography, compression, error-correction, databases, etc, the spec is often much simpler than the implementation.
I don't know why you created a new account for this, but take the textbook example of a nontrivial formally verified system: SeL4. That implementation was 8.7k of C code, which correspondend to 15k lines of Isabelle that ultimately needed 100k+ lines of proof to satisfy. And that was with the formal model excluding lots of important properties like hardware failure that actual systems deal with.
You are confusing the proof with the spec/theorem. A correct proof and a valid proof are the same thing. It doesn't really matter how long the proof is, and you don't even need to understand it for it to be correct, the machine can check that.
But indeed, if the spec includes 8.7k of C code, that is problematic. If you cannot look at the theorem and see that it is what you mean, that is a problem. That is why abstraction is so important; your ultimate spec should not include C-code, that is just too low-level.
I'm not confusing them. That's why I gave each of the numbers for SeL4 separately.
Knowing whether those theorems are the right theorems for the problem can be as difficult as understanding the implementation itself. Hence the example of SeL4 where the number of theorems exceeds lines of code in the original implementation and the formal model is large.
It's my experience that most people doing formal methods have seen cases where they actually proved something slightly different than what they intended to. This usually involves an unintentional assumption that isn't generally true.
I think you have been confusing them. Two theorems are the same if they have the same statement (spec). A proof is not a theorem, nobody cares about when two proofs are the same or not.
Yes, and if you have the wrong theorems, the proof doesn't matter. Verification vs validation. Proofs solve verification, but the hard problem of validation remains.
> I don't know why you created a new account for this
What value does this add to the conversation? I’m not seeing it: am I missing something? It comes across as a kind of insult.
They made a good point in my opinion! (The “Uhm no” part got it off on the wrong foot, I will admit.) But even if you felt annoyed or didn’t agree with the point, it was substantive and moved the conversation forward. I’m here for the (genuine) questions and (constructive) debate and (civil) pushback.
I like to welcome new users before they take too much of a beating. That can come later when they are too invested to leave and/or when morale needs improving.
So welcome! Bring a helmet, and don’t stop disagreeing.
The original point I was trying to make is the distinction between verification and validation. I'm a bit surprised it's been controversial, but maybe I expressed things poorly.
I talk to other people. They influence me, steer me. I am okay with that.
reply