anything particular you're thinking of?
Conversation
you know my first response was: i wish i could actually use formal approach in my work. this fermented into: maybe i should just stay away from work where this is not possible
1
because if i zoom in to what exactly made last couple of years so difficult, it is all about unpredictable hardware issues. "side problems"
1
and overall legacy things that are broken and can't be reasonably fixed
1
1
cant-fix-paint-over infinitely stacking tetris games
1
just a heads up spending time in proof assistants is probably the opposite of avoiding "infinitely stacking tetris games"
1
2
and infact, there are people who devote a major portion of their time in improving proof assistants by making the types as tetris-like as possible so that proofs stack more easily
1
1
the impression i got from the little i read is that proofs that say something useful are always going to be very large and composite in weird ways, and that typically you need a lot of metaprogramming to keep them manageable
Replying to
i only work with agda/tla+ so i can only speak for those language.
but what i was referring to was that the way you represent information in proof's subject is more important than the assertion the proof makes (usually)
1
1
this is more true in agda since the types are precisely the questions you care about asking.
mcbride recently talked about it here
1
1
Show replies