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 racket-users+unsubscr...@googlegroups.com. > 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/20190729161525.q4o3j2peguc5itdd%40topoi.pooq.com.
