Friday, September 18, 2009

Source Code File Separation

Why does java separate each public class into a different file?
C++ has no restrictions on this and we can freely include whatever we want in any file.

Whatever other abstractions are there to be separated into different files?

Teaching computer science with VDO games

I came across a paper "Why Computer Science Doesn't Matter" by Dr. Felleisen and Dr. Krishnamurthi (http://www.cs.brown.edu/~sk/Publications/Papers/Published/fk-why-cs-doesnt-matter/paper.pdf).

They talked about incorporating computer science into high-school math so it could be more easily understandable. In fact, I think computer science it also pretty much like solving puzzles, and if we can cross the line of formalism, pretty much anyone can reason about programming.

Could we teach computer science with VDO games?
If so, would the ideal programming language for high-schoolers be a VDO game?

Finding the best implementation and design

How would one go about finding the best way to implement something, given some constraints (the language must be JAVA, must use only int, and so on), using a SAT-solver?

Formal Language Translator

I've taken a model checking class. One subject that the instructor touched on was reducing problems to SAT and decision procedures.

For example, we can reduce a sudoku puzzle to a CNF to be solved by a SAT-solver. A variable x127 may represent "1 being at coordinate (2,7)".

When a SAT solves the problem, it tells us which variable has the truth value "true".

Without knowledge of reduction and using SAT-solvers, a normal programmer wouldn't be able to do this. What if we had a tool such that we can use an easier understanding language to state the problem and show the answer?

The tool should be able compile the easy language into intricate mathematics and translate it back to the easy language when we get the answer.

That would make learning reduction easier.

Thursday, April 9, 2009

What lies between model checking and static analysis

A fun conversation with my fellow students and a professor lead to a joke.

The professor said that there was a saying that for model checking, you give the model checker a problem and it never comes back. For static analysis, you give the system a problem and it comes back immediately saying, "I don't know".

That was a good joke.

So what's in between?

I think it should look like running a static analysis and when we don't know the answer, we run it a little bit then come back and try to answer again.

Friday, January 9, 2009

The end of model checking

I wonder what would happen if computers were so powerful that they could model check an untractable number of states within a small amount of time.

Would that make model checking techniques that emerged over the past century become useless?

Just like when memory became less and issue in object-oriented languages.
What would happen then?

Thursday, September 25, 2008

What's equivalent to a type system?

Today was my first "probability with poker" class.
There was something interesting the instructor said.
He brought up the Venn diagram while teaching probability.
He said that the reason we can use area and probability interchangeably was that they shared the same axioms, or as I understand, the same properties.

Last quarter in the static analysis class, a proof was also shown that the type checking problem was equivalent to some static analysis problem.

Three quarters ago, in the type system class, there was this Curry-Howard correspondence theory that shows that logic was somehow equivalent with programming languages.

Now it might be possible that type systems could be equivalent with geometry.
So when we type check, we see circles and squares floating around.

Who knows.