On Sun, Jul 28, 2019 at 05:03:16PM -0700, Atlas Atlas wrote: > пятница, 26 июля 2019 г., 23:35:45 UTC+3 пользователь Hendrik Boom написал: > > > > > One of the great things about Idris is its dependent types, and the > > way they can be used for (constructive) formal logic. I was > > experimenting with them in the 80's. > > > > To make them into a secure logic, however, you need limitations on > > recursion. You need to effectively and provably show that all > > recursions terminate. > > That's a tall order for a language like Lisp. > > > > Perhaps to be practical security can be sacrificed.
What really kills security is the possibility of nonterminating type expressions. > > > > > I like Gambit's approach of easily mixing Lisp and C. If only C > > implemented tail-recursions properly and had optional garbage > > collection. > > > > Or maybe we need more low-level operations and data structures in > > Racket 2. Modula 3, for example, manages to combine static > > type-security, garbage collection, systems-programming-style data > > structures, and an efficient code generator. > > > > Functional structs works really bad for me, as well as classes. > The main idea of struct is to simple combine some values together, in > simple way. (at leas as I see it) > Every time I try to use classes or structs I ending trashing all and use > plane datatypes. > I think racket classes can be useful for complex IO objects like databases, > GUI, or any UI, but I am not sure. > In some places Racket shows tremendous possibilities and high complexity, > and at the same time leaves some obvious things with small attention. > > About structs in regard of low level operations. > In C#, structs have option to alight data in specific order, what makes > possible for very effective data packaging in some cases. > For example I can encode in struct 4 bytes as 1 unsigned integer and have > access to each individual byte and to integer as whole. > This can be really handy sometimes. Yes. Very handy. -- hendrik > > > In racket I just cannot think as before, in concepts of int16\32\64, this > also questions for me possibility of effective algorithms realization. I still think in terms of limited size integers ehrn they are useful. I need types and operations that respect those types, have overflow detection, etc., and you I then use them if and only if they are appropriate for the application. When the application diesn't require them I prefer integers that get as large as they need to be. But in C/C++ programming on 32-bit machines, I find few cases where the available 32-bit integers don't suffice. But I hate C's default of no overflow detection. I like modulo-4294967296 arithmetic only when I specifically want it. -- hendrik > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/6b83862a-6f5d-438a-8a59-abffa5e6a94b%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/20190729161525.q4o3j2peguc5itdd%40topoi.pooq.com.
