Viewing a single comment thread. View all comments

Moonside wrote

I think Emacs must count for being very idiosyncratic, at the very least, even if it's well known. I wish it was more robust though.

CoqIDE is for the Coq theorem prover and using it has this weird video gamey vibe to it. When you're proving a theorem in Coq, you're essentially manipulating equations until they "match" the target one. In essence, you write a "sentence" in Coq - commands actually do end with periods, then hit the next step command and Coq checks whether your command compiles or not. If it does, your reasoning was valid in a way that Coq could verify. I think it would be possible to write a very good puzzle game along these lines, actually.

There's this fantasy video game console called Pico-8 that actually houses a development environment in itself, including a music sequencer, sprite editor and an editor. It uses Lua, which is honestly a bit too quirky a language for me.

Also any time there's an actually usable repl, it's both weird and quite welcome. Weird because they're rare, welcome because it's such a fast way of trying out things. But I do feel they could be loads better if they weren't subject to the idiosyncrasies of terminal emulators. Like setting up a custom prompt for each language is a lot of work for such a little thing. For GHCi (for Haskell), I have the current working directory, loaded modules and a pink lowercase lambda as my prompt which is cool since now I can distinguish between terminal windows at a glance, but of course I had to assimilate a bunch of tutorials all around the place to make it happen.

4

twovests OP wrote

oh man i gotta check out Coq, that sounds Really Rad tbh

i also definitely need to check out Pico 8 someday (i blame you oakreef for this interest)

2