Hi Jiri,
going back to our debate. To make the email shorter, if I don't comment
on something explicitly I consider it reasonable.
To make this simpler, I am currently trying to avoid global variables
completely. They will not be supported by the first iteration of the
language. Whether or not that is a practical approach is open for debate.
Well, sometimes you just cannot avoid dealing with the global state of
the program -- especially if you think about the kernel which is not a
computable function, but rather an endlessly running automaton. If you
don't have global variables, you still need something else that would
represent the global state.
The question is whether global variables are not the most
straightforward representation of the global state or whether
encapsulating the global state into something else is beneficial.
By the way, I expect an argument of the form that the static type should
not depend on complicated analysis of condition expressions. I agree.
You can, however, only interpret for type annotations a certain form of
expressions, put those expressions in there as assertions, and let the
SMT solver prove (or disprove, or timeout for) the rest.
Yes, but the concern that remains is that the SMT solver might timeout
in many non-trivial cases. To what extent should the core language rely
the SMT solver and to what extent should be easier formal verification
only a bonus.
Things like alignment and endianity can be present in the form of
user-provided attributes, instead of something predefined.
Yes, sure. I don't expect "uint32_aligned_little_endian_t" to be a
built-in type of the language. I used it only as a way to express my idea :)
Definitely a good idea, with "some kind" being the biggest problem. I
don't really know how to go about it right now. If someone can create
(or adapt from another language that already has) a nice and sane
system, I am buying that person a few rounds of beer.
I am not aspiring for the beers, but I would start with C++ function
templates (not class templates) and limiting the concept further to
avoid some nasty corner cases.
Basically the end-user wants the freedom of C macros and the author
wants static (abstract) type checking.
- type system with support for physical dimensions (e.g. m*s^-2, bytes,
pages = bytes/PAGE_SIZE, etc.), ideally with safety assignment checks
or explicit conversion functions
That is not really useful for the purpose I am aiming for, I think.
Well, in my opinion this might help to avoid many trivial, but hard to
debug bugs, because it gives the compiler the information that not all
scalar types and values are equal.
You could statically check that the assignments respect the magnitude
and dimensions of the types. As in physics you should not be allowed to
assign length in metres to a variable representing force in newtons.
I'd rather completely avoid implicit calls to user-defined functions. I
might change my mind if I see it improves readability, but I have a
feeling it would hurt it (code lying to the reader by omission).
OK, sounds fine. In that case I would also avoid any kind of implicit
type conversions -- even the trivial ones such as promoting uint16_t to
uint32_t.
This might render the code a little bit too verbose in the end, but
better safe than sorry.
Please do. :)
I'll pass for now. I hope that you don't plan to freeze the
specification of your new language in the very moment you release it.
Thus elaborating on your first prototype after you release it is perhaps
better than building castles in the sky now.
M.D.
_______________________________________________
HelenOS-devel mailing list
[email protected]
http://lists.modry.cz/listinfo/helenos-devel
