lower

I've spent so much time for pointless reformatting. With Springer LNCS it's often that you have to work really hard to cram everything into the page limit. Then Springer does some editing in the bibliography, and the article then often overflows by one or two bibliography entries and is published like that, making the effort of meeting the page limit a complete waste time

We've had various examples like these:

- Puzzles: Sudoku, St8ts

- Bridge crossing: Missionaries and cannibals, 17 minute bridge crossing (I need a computer to solve this anyway)

- Concurrency: finding bug in mutual exclusion algorithm (Peterson algorithm with a bug)

- Graphs: coloring a map, finding a Hamilton path

- Sorting: Finding bugs in a sorting network

For many students it was difficult to encode problems in SAT. They seemed to understand given example encodings, but then found it difficult to vary them. There is a lot of freedom in how one may encode things and it's hard at first to debug at first when things don't work in the way you're expecting. If there is no solution, then one needs to investigate where there are unwanted constraints or errors in the encoding. If there are unwanted solutions, one needs to identify the missing constraints. It was hard to get across how to do this and it's probably frustrating for beginners.

I used to teach formal methods at university, including a course with a lot of SAT examples. We tried to make it as practical as possible, with many examples and exercises in Java (where you just generate your formulas and call a solve method). Thing is, most students seemed to hate it passionately, just like with reductions to SAT in complexity theory.

Yeah, but then you have: It seems like every week or two this year, another crisis presented itself, each manageable in isolation.

I've had this happen and it really grinds you down when you work full-out for months and, just when you think you've contained all the crises, the next one drops.

> But the professor said he'd never do it again because 30 minutes * 30ish students was too much work.

The old German Diplom system (replaced by BSc/MSc about 15 years ago) was based on oral exams. The way this worked there was that there were much fewer exams. For example, in Computer Science I had my first oral exams two years into the degree, and there were only five of them: one in Mathematics, one in each of Theoretical, Practical and Applied, Computer Science, and one for the second subject. Each of these oral exam was 30 minutes but covered the content of four semesters. There was a second round of such exams at the end of the degree and that was it.

To be admitted to an oral exam, one needed to pass the courses that the exam was going to be about. Lecturer were free to set the passing requirements. It was often just something like a coursework threshold of 60%.

There exist only two kinds of modern mathematics books: ones which you cannot read beyond the first page and ones which you cannot read beyond the first sentence. -- Chen Ning Yang

It's interesting that OCaml's syntactic quirks go back to Edinburgh ML. I had never known about this bit of history.

~/Repos of course

It's the Holy Roman Empire of modern times.