?

Log in

No account? Create an account
"should be" - Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

[ website | composition.al ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

"should be" [Feb. 22nd, 2010|06:01 pm]
Lindsey Kuper
[Tags|, , ]

I used to be nervous about holding office hours, because I thought that students would ask me difficult questions and that I would be revealed as a fraud when I couldn't answer them. Today, though, after trying to reason about dependent types until I felt as though my brain had been liquefied, and then going to class and trying to reason about non-axiomatizable classes of structures1, it was incredibly relaxing and refreshing to go talk to my students for a while. If nothing else, it's a reminder of how far I've come in a year. A year ago, I didn't understand all of the stuff I'm helping them learn now.

I did have to look up one thing to help answer a student's question. But I was proud that I knew exactly what book to grab off the shelf and, furthermore, exactly what page to turn to. Ninety percent of success is knowing where to look things up.

I asked one of my students if his code was working, and he replied, "It should be working." I think I like this "should be" thing quite a lot. Next time my supervisor asks me how my projects are going, I'll cheerfully say, "They should be going great!"


  1. This is for a course called "Introduction to Applied Logic". I can't imagine what they talk about in Introduction to Theoretical Logic.
LinkReply

Comments:
[User Picture]From: jes5199
2010-02-22 11:10 pm (UTC)

reminds me

Markus: I think this problem might have become undeterminable, turing-complete.
Me: Oh, yeah, it definitely is.
Markus: "Definitely"?!
Me: Well, you have to understand that when I say 'definitely' I mean that I'm jumping wildly between intuitions
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-02-23 12:23 am (UTC)

Re: reminds me

Ooh, can I see the problem?

Dependent type checking is undecidable, which sounds like Bad Idea Jeans, but in practice, it isn't so bad; you can always cut the typechecker off and have it ask you for more information if it's thrashing.
(Reply) (Parent) (Thread)
[User Picture]From: jes5199
2010-02-23 12:39 am (UTC)

Re: reminds me

this is probably related to dependent type checking, but it's on a different level of abstraction

we've got a home-baked programming language. it's (supposed to be) immutable, and we're making it lazily-evaluated and order-independent

but we also want to add Dictionaries to the language (we're ruby geeks so we call them 'Hashes'), and so we've hit a problem: the keys to a dictionary are strings, and strings are lazily evaluated, and strings may be stored in dictionaries.
So someone might declare something like:
$hash[ $hash[ "a" ] ] = $hash["b"]
and if $hash["a"] is declared elsewhere, we're cool, but if not, $hash[ $hash[ "a" ] ] waits forever, because the outer $hash[] is waiting for the inner one to resolve, and the inner one is waiting for all of the possible $hash[] definitions to be resolved so it can definitively return undefined
(Reply) (Parent) (Thread)
[User Picture]From: jes5199
2010-02-23 11:20 pm (UTC)

Re: reminds me

I really am interested in your thoughts on this, even if it's just 'gah! that's weird!'
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2010-02-25 12:57 am (UTC)

Re: reminds me

I want to answer so badly, but this week is hell. I had a project proposal due today and I'm trying to get a talk ready for tomorrow. Soon, though!
(Reply) (Parent) (Thread)
[User Picture]From: lyceum_arabica
2010-02-23 05:10 pm (UTC)
yeah, I gather from mark's tales last year that levant's applied logic class isn't. Makes me wonder if 'applied' is a technical term for logicians that means something completely other than "put to useful ends".
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-02-24 03:37 am (UTC)
You'd have to ask a logician. But Larry Moss has an article called "Applied Logic: A Manifesto" that might explain what people mean by it, or at least what he thinks they should mean.
(Reply) (Parent) (Thread)