Hm, honestly I need a version of Agda with no unicode support, no holes, no implicit arguments, and so on for the sake of teaching
15
2
50
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Agda with no holes isn't Agda, I agree. It's a very pale shadow of Agda, with all the fun taken out.
1
11
But holes confuse the hell out of students, especially with the awful keybindings for dealing with them, which half the time don't even work on Macs
4
1
I use Agda on a Mac 99% of the time, no problem. Had to learn emacs because of it. Yes, a hurdle, but worth it.
Students are confused by holes because they have to UNLEARN too many things they take for granted about programming. Unlearning is very hard.
2
2
I used emacs to write my PhD thesis but that was in 1995. Do you people working in CS departments really still expect students to have to learn emacs with all its weird nonstandard keybindings in 2022? For me this is cruelty. My students use VS Code.
4
6
That's like asking a painter why they still use paint brushes when all the kids do just fine with spray cans.
Power tools only reveal themselves to those who spend the time to learn their craft. But then, the things they can do with those tools!
2
3
This is a bad argument for Emacs, it always has been, and it's an especially bad argument in 2022 where VSCode is extensible, free, and available everywhere.
3
1
7
I'll need to give VSCode another try. I have tried it in the past. It was way too slow to start up (though nothing compared to Eclipse and others of its ilk - them, I just delete) and took up too much screen real estate with useless crap.
2
2
You can customize this stuff in VSCode. There's even a super-minimal "zen mode".
1
2
Yeah you can turn off a bunch of stuff like the minimap, tab bar, sidebars etc. (also change their locations)