new tablet PC
Apr. 9th, 2008 06:10 amI'm writing this from my new tablet PC! Woo hoo!
Apr. 9th, 2008
tablet PC desiderata
Apr. 9th, 2008 10:18 pm* a block/pad to hold it diagonal
* writing notes on PDFs (buy this?)
* free writing, instead of line-by-line. I find myself looking for tiny buttons like "bksp" and "space", a little too often. OneNote does have that feature, but it's cumbersome to change windows, and you lose the context this way.
* It does not recognize Portuguese characters
the handwriting recognition is way better than Dragon's speech recognition. OTOH, I do not have a super mic on my low-end headset.
* writing notes on PDFs (buy this?)
* free writing, instead of line-by-line. I find myself looking for tiny buttons like "bksp" and "space", a little too often. OneNote does have that feature, but it's cumbersome to change windows, and you lose the context this way.
* It does not recognize Portuguese characters
the handwriting recognition is way better than Dragon's speech recognition. OTOH, I do not have a super mic on my low-end headset.
I think I haven't been claiming my 401(k) contributions for the past several years. Every year, my employer sends me a W2 and my bank sends me a 1099, but my IRAs never send me anything. Am I supposed to keep track of my yearly contributions by myself? How many years can I put this off, before I can claim them all at once?
type theory
Apr. 9th, 2008 11:42 pmI really sympathize with type theory folks' (or, at least ![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
jcreed's) desire for using type theory in common discourse. After Risi Kondor's lecture today, type theory made it possible for us to communicate formally and efficiently.
For example, the Fourier Transform on permutation groups
^ : (Perm -> Reals) -> (Repr -> Reals)
which is analogous to the regular FT
^ : (Time -> Reals) -> (Frequency -> Reals)
the function f : Graph x Perm -> {0,1} encodes whether there is an edge between the last two nodes in the permutation.
I want some sort of editor for helping me formalize natural language statements of a technical nature. Such formalization seems like a very good exercise when you're not familiar with the ideas and you're trying to see how they fit together. Still, I'm not sure exactly what features I'd want it for. Type inference (e.g.: SOLVED! "Blicket" is an instance of "Vehicle")? Catching fallacious or ill-formed statements? Automatic metonymy detection?
jcreed's) desire for using type theory in common discourse. After Risi Kondor's lecture today, type theory made it possible for us to communicate formally and efficiently.For example, the Fourier Transform on permutation groups
^ : (Perm -> Reals) -> (Repr -> Reals)
which is analogous to the regular FT
^ : (Time -> Reals) -> (Frequency -> Reals)
the function f : Graph x Perm -> {0,1} encodes whether there is an edge between the last two nodes in the permutation.
I want some sort of editor for helping me formalize natural language statements of a technical nature. Such formalization seems like a very good exercise when you're not familiar with the ideas and you're trying to see how they fit together. Still, I'm not sure exactly what features I'd want it for. Type inference (e.g.: SOLVED! "Blicket" is an instance of "Vehicle")? Catching fallacious or ill-formed statements? Automatic metonymy detection?