if you want to reinvent the agda editor experience (or have smaller ideas for how it could be improved atm), please reach out - usability is the #1 thing on my head. even if i'm focused on improving cubical, the rest of the language needs to be better, too :)
Conversation
Honestly, buttons would go incredibly far, the keybinding approach to things is extremely counterintuitive to most students (and me, honestly)
2
7
I read Talia's post and my first thought was "y'all need language levels".
Of course, we DO have an awesome formal methods tool with language levels, y'all just won't use it <-;. [Insert "proof theory people will literally … just to avoid …" joke here.]
1
15
Language levels is exactly where my mind went when I was reading the discussion on holes
1
5
We said this in 1997, and it'll be just as true in 2097. Every non-trivial language needs language levels, some are just slower to accept it and even slower to implement it than others.
read image description
ALT
3
2
24
I believe it.
I imagine it's also difficult to convince students of their value: I learned Racket with language levels, and in retrospect, it really forced me to understand what was happening, but at the time I just wanted to steamroll ahead to more exciting features.
1
6
Yeah, even starting with Agda is a way of pretending I have language levels? Because next exercise we do some of the same proofs in Coq, this time with access to tactics
1
8
If I could disable tactics entirely in Coq before adding them in, I'd love that. I really don't like how people think about proofs when they learn tactics before proof objects, be they ephemeral or explicit
1
12
Then everyone just games proofs, and this really makes things much harder later on
1
8
Like super weird how many courses teach you metaprogramming via tactics before you learn the actual programming language you're doing metaprogramming for ...
2
1
22
Personally I liked using Agda, Lean, and Idris first, just doing pattern matching and recursion as tactics were always too confusing to me. Later after looking into Lean’s implementations of tactics, and stuff like bentnib.org/posts/2015-04- the tactics stuff clicked more.
I agree learning to prove things without tactics makes for a better way to understand what is going on.
Tactics although convenient always made things opaque for me.
One of the reason I am enjoying agda.
Also I get really confused by the semantics of how some tactics are used
1
2
Also when I'm talking about semantics I'm talking about usage semantics where some tactics can use `by` and there are things like `[easy|]` when I want to use it on the first constructor and `[easy..|]` when I want to use on all constructors except the last.
Maybe I suck at it.
1
Show replies