Statement for the 21st Century Engineering Consortium Workshop

Ganesh Gopalakrishnan
Department of Computer Science
University of Utau
March 1998

- The feeling that system design "can be done without the aid
  of Mathematical Logic" is too deeply entrenched into the CS
  "culture". DARPA funding for big systems projects can, with
  a modest shift in emphasis, help ameliorate this situation.
  For instance, when DARPA funds large computer architecture /
  OS / software-engineering grants, why not require FM to be
  integrated into whatever gets built? My own FM research efforts
  got such a boost thanks to actual designs and NDAs made possible
  by a big DARPA grant that some of my colleagues got - but
  unfortunately, the project timetables didn't allow our "big-project
  inspired FM ideas" to be actually applied to the direct benefit
  of the big-project itself. (Well, it could have, but then most
  of us know what happened to that hardware verification BAA 96-07 under
  which I was hoping to make the tech-transfer happen...)
  So I propose that DARPA can get more for what it already invests
  with the above emphasis added to systems BAAs. Also dedicated
  BAAs for FM education can't hurt :-).

  It is also time we thought about how to define "success" and "progress",
  using the quality axis for a change (not just "fast" "fast" - see
  the current mindset expressed in Kahan's quote reproduced in
  the Hennessy/Patterson book - "fast things
  will supercede slow things even if they are wrong!).

- I think that undergrads do love formal stuff. I've not taught too
  many UG classes - and this time when I did, I found them really
  enjoying the precision formal stuff has! I was surprised!

  Of course they often see formal stuff so late, so hurried, etc.
  I've learnt a great deal from  the writings of researchers like
  Vardi who can explain things
  the automata-theoretic way so nicely. This time when I taught
  automata theory from Sipser's book (I can't wait to read that
  book cover to cover), I could show the students how Presburger
  decision can be done by DFAs. Sipser covers it nicely. Using this
  trick, one of us has "taught" SPIN to do Presburger decision, and
  my students did try that. Alas time ran out before full enjoyment
  could be derived.

  Bottom-line: we need a repository (a vault) for
  the gems of pedagogy that we all shall contribute to. Steve Johnson's
  dissertation also has some nice insights that ought to be more
  widely known. I'm sure there are tons more of examples - what I'm
  saying is that if we can collect the gems of pedagogy falling
  into systems areas, they can be more widely shared / used / improved.

- I've learned from Shiu-Kai that FM can be viewed as formal modeling,
  formal analysis of the models, and predicting system behavior. I've
  experienced positive reaction when I myself tried touting this
  Engineering view.

- Ultimately we want "just in time math" as Doug Troeger would say.