A colleague of mine once taught a formal methods course for students working on their masters -- not beginners by any stretch.

The exercise was to implement binary search given the textbook specification without any errors. An algorithm they had probably implemented in their first-year algorithms course at the very least. The students could write any tests they liked and add any assertions they thought would be useful. My colleague verified each submission against a formal specification. The majority of submission contained errors.

For a simple algorithm that a student at that level could be reasonably expected to know well!

Now... ChatGPT and other LLM-based systems, as far as I understand, cannot do formal reasoning on their own. It cannot tell you, with certainty, that your code is correct with regards to a specification. And it can't tell you if your specification contains errors. So what are students learning using these tools?